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 $ *)
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".
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:
inline "cic:/CoRN/tactics/GroupReflection/Tactic_lemmaG.con".
(* UNEXPORTED
-End Group_NormCorrect.
+End Group_NormCorrect
*)
(* end hide *)