include "tactics/AlgReflection.ma".
(* UNEXPORTED
-Section Ring_Interpretation_Function.
+Section Ring_Interpretation_Function
*)
-inline "cic:/CoRN/tactics/RingReflection/R.var".
+alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/R.var".
-inline "cic:/CoRN/tactics/RingReflection/val.var".
+alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/val.var".
-inline "cic:/CoRN/tactics/RingReflection/unop.var".
+alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/unop.var".
-inline "cic:/CoRN/tactics/RingReflection/binop.var".
+alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/binop.var".
-inline "cic:/CoRN/tactics/RingReflection/pfun.var".
+alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/pfun.var".
inline "cic:/CoRN/tactics/RingReflection/interpR.ind".
inline "cic:/CoRN/tactics/RingReflection/interpR_wd.con".
(* UNEXPORTED
-End Ring_Interpretation_Function.
+End Ring_Interpretation_Function
*)
(* UNEXPORTED
-Section Ring_NormCorrect.
+Section Ring_NormCorrect
*)
-inline "cic:/CoRN/tactics/RingReflection/R.var".
+alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/R.var".
-inline "cic:/CoRN/tactics/RingReflection/val.var".
+alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/val.var".
-inline "cic:/CoRN/tactics/RingReflection/unop.var".
+alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/unop.var".
-inline "cic:/CoRN/tactics/RingReflection/binop.var".
+alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/binop.var".
-inline "cic:/CoRN/tactics/RingReflection/pfun.var".
+alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/pfun.var".
(* NOTATION
Notation II := (interpR R val unop binop pfun).
inline "cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con".
(* UNEXPORTED
-End Ring_NormCorrect.
+End Ring_NormCorrect
*)
(* end hide *)