X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftactics%2FGroupReflection.ma;h=e47a4cf2ebc05c01fa7a07c5cd2bcc714fd489f3;hb=09c8bb55c25143efdfbd34a20bb2fe6b681760b6;hp=6c9924caf36c2b406ddabf450b939bb9ac904551;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;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 6c9924caf..e47a4cf2e 100644
--- a/helm/software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/tactics/GroupReflection".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: GroupReflection.v,v 1.3 2004/04/23 10:01:06 lcf Exp $ *)
 
@@ -27,18 +27,18 @@ include "algebra/CAbGroups.ma".
 include "tactics/AlgReflection.ma".
 
 (* UNEXPORTED
-Section Group_Interpretation_Function.
+Section Group_Interpretation_Function
 *)
 
-inline "cic:/CoRN/tactics/GroupReflection/G.var".
+alias id "G" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/G.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/val.var".
+alias id "val" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/val.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/unop.var".
+alias id "unop" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/unop.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/binop.var".
+alias id "binop" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/binop.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/pfun.var".
+alias id "pfun" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/pfun.var".
 
 inline "cic:/CoRN/tactics/GroupReflection/interpG.ind".
 
@@ -129,22 +129,26 @@ inline "cic:/CoRN/tactics/GroupReflection/refl_interpG.con".
 inline "cic:/CoRN/tactics/GroupReflection/interpG_wd.con".
 
 (* UNEXPORTED
-End Group_Interpretation_Function.
+End Group_Interpretation_Function
 *)
 
 (* UNEXPORTED
-Section Group_NormCorrect.
+Section Group_NormCorrect
 *)
 
-inline "cic:/CoRN/tactics/GroupReflection/G.var".
+alias id "G" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/G.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/val.var".
+alias id "val" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/val.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/unop.var".
+alias id "unop" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/unop.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/binop.var".
+alias id "binop" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/binop.var".
 
-inline "cic:/CoRN/tactics/GroupReflection/pfun.var".
+alias id "pfun" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/pfun.var".
+
+(* NOTATION
+Notation II := (interpG G val unop binop pfun).
+*)
 
 (*
 four kinds of exprs:
@@ -235,7 +239,7 @@ inline "cic:/CoRN/tactics/GroupReflection/NormG_corr_G.con".
 inline "cic:/CoRN/tactics/GroupReflection/Tactic_lemmaG.con".
 
 (* UNEXPORTED
-End Group_NormCorrect.
+End Group_NormCorrect
 *)
 
 (* end hide *)