X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftactics%2FGroupReflection.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftactics%2FGroupReflection.ma;h=e47a4cf2ebc05c01fa7a07c5cd2bcc714fd489f3;hb=55444711ececb62f0a93f2a064f64c3b27f744e2;hp=c314cc08968d84c20d8988ad80aa6195d67bcfc4;hpb=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma b/helm/software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
index c314cc089..e47a4cf2e 100644
--- a/helm/software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
@@ -30,15 +30,15 @@ include "tactics/AlgReflection.ma".
 Section Group_Interpretation_Function
 *)
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/G.var" "Group_Interpretation_Function__".
+alias id "G" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/G.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/val.var" "Group_Interpretation_Function__".
+alias id "val" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/val.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/unop.var" "Group_Interpretation_Function__".
+alias id "unop" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/unop.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/binop.var" "Group_Interpretation_Function__".
+alias id "binop" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/binop.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/pfun.var" "Group_Interpretation_Function__".
+alias id "pfun" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/pfun.var".
 
 inline "cic:/CoRN/tactics/GroupReflection/interpG.ind".
 
@@ -136,15 +136,15 @@ End Group_Interpretation_Function
 Section Group_NormCorrect
 *)
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/G.var" "Group_NormCorrect__".
+alias id "G" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/G.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/val.var" "Group_NormCorrect__".
+alias id "val" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/val.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/unop.var" "Group_NormCorrect__".
+alias id "unop" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/unop.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/binop.var" "Group_NormCorrect__".
+alias id "binop" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/binop.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/pfun.var" "Group_NormCorrect__".
+alias id "pfun" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/pfun.var".
 
 (* NOTATION
 Notation II := (interpG G val unop binop pfun).