...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / tactics / RingReflection.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma b/helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma
index 1e0fa25dc325f87734efc469078430e808de4e2c..d51f1688706acd4ebebc511ee4359160985165d7 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma
@@ -28,47 +28,57 @@ include "tactics/AlgReflection.ma".
 Section Ring_Interpretation_Function
 *)
 
-alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/R.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/R.var
+*)
 
-alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/val.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/val.var
+*)
 
-alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/unop.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/unop.var
+*)
 
-alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/binop.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/binop.var
+*)
 
-alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/pfun.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/pfun.var
+*)
 
 inline procedural "cic:/CoRN/tactics/RingReflection/interpR.ind".
 
-inline procedural "cic:/CoRN/tactics/RingReflection/wfR.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/wfR.con" as definition.
 
 inline procedural "cic:/CoRN/tactics/RingReflection/xexprR.ind".
 
-inline procedural "cic:/CoRN/tactics/RingReflection/xforgetR.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/xforgetR.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/xinterpR.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/xinterpR.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/xexprR2interpR.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/xexprR2interpR.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/xexprR_diagram_commutes.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/xexprR_diagram_commutes.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/xexprR2wfR.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/xexprR2wfR.con" as lemma.
 
 inline procedural "cic:/CoRN/tactics/RingReflection/fexprR.ind".
 
-inline procedural "cic:/CoRN/tactics/RingReflection/fexprR_var.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/fexprR_var.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/fexprR_int.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/fexprR_int.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/fexprR_plus.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/fexprR_plus.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/fexprR_mult.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/fexprR_mult.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/fforgetR.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/fforgetR.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/fexprR2interp.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/fexprR2interp.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/fexprR2wf.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/fexprR2wf.con" as lemma.
 
 (* UNEXPORTED
 Opaque csg_crr.
@@ -138,9 +148,9 @@ Opaque cr_mult.
 Opaque nexp_op.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/refl_interpR.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/refl_interpR.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/interpR_wd.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/interpR_wd.con" as lemma.
 
 (* UNEXPORTED
 End Ring_Interpretation_Function
@@ -150,15 +160,25 @@ End Ring_Interpretation_Function
 Section Ring_NormCorrect
 *)
 
-alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/R.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/R.var
+*)
 
-alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/val.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/val.var
+*)
 
-alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/unop.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/unop.var
+*)
 
-alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/binop.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/binop.var
+*)
 
-alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/pfun.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/pfun.var
+*)
 
 (* NOTATION
 Notation II := (interpR R val unop binop pfun).
@@ -182,7 +202,7 @@ P: sorted on M, all M's not an I
 Opaque Zmult.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/MI_mult_corr_R.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/MI_mult_corr_R.con" as lemma.
 
 (* UNEXPORTED
 Transparent Zmult.
@@ -192,7 +212,7 @@ Transparent Zmult.
 Opaque MI_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/MV_mult_corr_R.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/MV_mult_corr_R.con" as lemma.
 
 (* UNEXPORTED
 Transparent MI_mult.
@@ -202,7 +222,7 @@ Transparent MI_mult.
 Opaque MV_mult MI_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/MM_mult_corr_R.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/MM_mult_corr_R.con" as lemma.
 
 (* UNEXPORTED
 Transparent MV_mult MI_mult.
@@ -212,7 +232,7 @@ Transparent MV_mult MI_mult.
 Opaque MV_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/MM_plus_corr_R.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/MM_plus_corr_R.con" as lemma.
 
 (* UNEXPORTED
 Transparent MV_mult.
@@ -222,7 +242,7 @@ Transparent MV_mult.
 Opaque MM_plus.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con" as lemma.
 
 (* UNEXPORTED
 Transparent MM_plus.
@@ -232,7 +252,7 @@ Transparent MM_plus.
 Opaque PM_plus.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/PP_plus_corr_R.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/PP_plus_corr_R.con" as lemma.
 
 (* UNEXPORTED
 Transparent PM_plus.
@@ -242,13 +262,13 @@ Transparent PM_plus.
 Opaque PM_plus MM_mult MI_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/PM_mult_corr_R.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/PM_mult_corr_R.con" as lemma.
 
 (* UNEXPORTED
 Opaque PM_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/PP_mult_corr_R.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/PP_mult_corr_R.con" as lemma.
 
 (*
 Transparent PP_plus PM_mult PP_mult PM_plus MI_mult.
@@ -310,9 +330,9 @@ Step_final x2.
 Qed.
 *)
 
-inline procedural "cic:/CoRN/tactics/RingReflection/NormR_corr.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/NormR_corr.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con".
+inline procedural "cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con" as lemma.
 
 (* UNEXPORTED
 End Ring_NormCorrect