1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/tactics/FieldReflection".
19 (* $Id: FieldReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
32 Section Field_Interpretation_Function.
35 inline cic:/CoRN/tactics/FieldReflection/F.var.
37 inline cic:/CoRN/tactics/FieldReflection/val.var.
39 inline cic:/CoRN/tactics/FieldReflection/unop.var.
41 inline cic:/CoRN/tactics/FieldReflection/binop.var.
43 inline cic:/CoRN/tactics/FieldReflection/pfun.var.
45 inline cic:/CoRN/tactics/FieldReflection/interpF.ind.
47 inline cic:/CoRN/tactics/FieldReflection/wfF.con.
49 inline cic:/CoRN/tactics/FieldReflection/xexprF.ind.
51 inline cic:/CoRN/tactics/FieldReflection/xforgetF.con.
53 inline cic:/CoRN/tactics/FieldReflection/xinterpF.con.
55 inline cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con.
57 inline cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con.
59 inline cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con.
61 inline cic:/CoRN/tactics/FieldReflection/fexprF.ind.
63 inline cic:/CoRN/tactics/FieldReflection/fexprF_var.con.
65 inline cic:/CoRN/tactics/FieldReflection/fexprF_int.con.
67 inline cic:/CoRN/tactics/FieldReflection/fexprF_plus.con.
69 inline cic:/CoRN/tactics/FieldReflection/fexprF_mult.con.
71 inline cic:/CoRN/tactics/FieldReflection/fforgetF.con.
73 inline cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con.
75 inline cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con.
81 inline cic:/CoRN/tactics/FieldReflection/refl_interpF.con.
83 inline cic:/CoRN/tactics/FieldReflection/interpF_wd.con.
86 End Field_Interpretation_Function.
90 Section Field_NormCorrect.
93 inline cic:/CoRN/tactics/FieldReflection/F.var.
95 inline cic:/CoRN/tactics/FieldReflection/val.var.
97 inline cic:/CoRN/tactics/FieldReflection/unop.var.
99 inline cic:/CoRN/tactics/FieldReflection/binop.var.
101 inline cic:/CoRN/tactics/FieldReflection/pfun.var.
114 P: sorted on M, all M's not an I
121 inline cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con.
131 inline cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con.
138 Opaque MV_mult MI_mult.
141 inline cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con.
144 Transparent MV_mult MI_mult.
151 inline cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con.
161 inline cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con.
171 inline cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con.
178 Opaque PM_plus MM_mult MI_mult.
181 inline cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con.
187 inline cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con.
190 Transparent PP_plus PM_mult PP_mult PM_plus MI_mult.
193 inline cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con.
195 inline cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con.
201 inline cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con.
203 inline cic:/CoRN/tactics/FieldReflection/NormF_corr.con.
205 inline cic:/CoRN/tactics/FieldReflection/Norm_wfF.con.
207 inline cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con.
209 inline cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con.
211 inline cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con.
214 End Field_NormCorrect.