inline procedural "cic:/CoRN/tactics/FieldReflection/interpF.ind".
-inline procedural "cic:/CoRN/tactics/FieldReflection/wfF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/wfF.con" as definition.
inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF.ind".
-inline procedural "cic:/CoRN/tactics/FieldReflection/xforgetF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xforgetF.con" as definition.
-inline procedural "cic:/CoRN/tactics/FieldReflection/xinterpF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xinterpF.con" as definition.
-inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con" as definition.
-inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con" as lemma.
inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF.ind".
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_var.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_var.con" as definition.
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_int.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_int.con" as definition.
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_plus.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_plus.con" as definition.
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_mult.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_mult.con" as definition.
-inline procedural "cic:/CoRN/tactics/FieldReflection/fforgetF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fforgetF.con" as definition.
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con" as lemma.
include "tactics/Opaque_algebra.ma".
-inline procedural "cic:/CoRN/tactics/FieldReflection/refl_interpF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/refl_interpF.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/interpF_wd.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/interpF_wd.con" as lemma.
(* UNEXPORTED
End Field_Interpretation_Function
Opaque Zmult.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con" as lemma.
(* UNEXPORTED
Transparent Zmult.
Opaque MI_mult.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con" as lemma.
(* UNEXPORTED
Transparent MI_mult.
Opaque MV_mult MI_mult.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con" as lemma.
(* UNEXPORTED
Transparent MV_mult MI_mult.
Opaque MV_mult.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con" as lemma.
(* UNEXPORTED
Transparent MV_mult.
Opaque MM_plus.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con" as lemma.
(* UNEXPORTED
Transparent MM_plus.
Opaque PM_plus.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con" as lemma.
(* UNEXPORTED
Transparent PM_plus.
Opaque PM_plus MM_mult MI_mult.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con" as lemma.
(* UNEXPORTED
Opaque PM_mult.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con" as lemma.
(* UNEXPORTED
Transparent PP_plus PM_mult PP_mult PM_plus MI_mult.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con" as lemma.
(* UNEXPORTED
Transparent FF_div.
*)
-inline procedural "cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/NormF_corr.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/NormF_corr.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/Norm_wfF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/Norm_wfF.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con" as lemma.
-inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con" as lemma.
(* UNEXPORTED
End Field_NormCorrect