X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FRefSeparated.ma;h=186466579fe76361af94e195d7ac1960fc68a967;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=a65a4ecdad1a6457e6efcabf6e7a5f29166a2381;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma index a65a4ecda..186466579 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma @@ -16,155 +16,153 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSeparated". +include "CoRN.ma". + (* $Id: RefSeparated.v,v 1.8 2004/04/23 10:01:00 lcf Exp $ *) (* begin hide *) -(* INCLUDE -COrdLemmas -*) +include "ftc/COrdLemmas.ma". -(* INCLUDE -Partitions -*) +include "ftc/Partitions.ma". (* UNEXPORTED Section Separating__Separated. *) -inline cic:/CoRN/ftc/RefSeparated/a.var. +inline "cic:/CoRN/ftc/RefSeparated/a.var". -inline cic:/CoRN/ftc/RefSeparated/b.var. +inline "cic:/CoRN/ftc/RefSeparated/b.var". -inline cic:/CoRN/ftc/RefSeparated/Hab.var. +inline "cic:/CoRN/ftc/RefSeparated/Hab.var". -inline cic:/CoRN/ftc/RefSeparated/I.con. +inline "cic:/CoRN/ftc/RefSeparated/I.con". -inline cic:/CoRN/ftc/RefSeparated/F.var. +inline "cic:/CoRN/ftc/RefSeparated/F.var". -inline cic:/CoRN/ftc/RefSeparated/contF.var. +inline "cic:/CoRN/ftc/RefSeparated/contF.var". -inline cic:/CoRN/ftc/RefSeparated/incF.var. +inline "cic:/CoRN/ftc/RefSeparated/incF.var". -inline cic:/CoRN/ftc/RefSeparated/Hab'.var. +inline "cic:/CoRN/ftc/RefSeparated/Hab'.var". -inline cic:/CoRN/ftc/RefSeparated/m.var. +inline "cic:/CoRN/ftc/RefSeparated/m.var". -inline cic:/CoRN/ftc/RefSeparated/n.var. +inline "cic:/CoRN/ftc/RefSeparated/n.var". -inline cic:/CoRN/ftc/RefSeparated/P.var. +inline "cic:/CoRN/ftc/RefSeparated/P.var". -inline cic:/CoRN/ftc/RefSeparated/R.var. +inline "cic:/CoRN/ftc/RefSeparated/R.var". -inline cic:/CoRN/ftc/RefSeparated/HP.var. +inline "cic:/CoRN/ftc/RefSeparated/HP.var". -inline cic:/CoRN/ftc/RefSeparated/HR.var. +inline "cic:/CoRN/ftc/RefSeparated/HR.var". -inline cic:/CoRN/ftc/RefSeparated/RS_pos_n.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_pos_n.con". -inline cic:/CoRN/ftc/RefSeparated/RS_pos_m.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_pos_m.con". -inline cic:/CoRN/ftc/RefSeparated/alpha.var. +inline "cic:/CoRN/ftc/RefSeparated/alpha.var". -inline cic:/CoRN/ftc/RefSeparated/Halpha.var. +inline "cic:/CoRN/ftc/RefSeparated/Halpha.var". -inline cic:/CoRN/ftc/RefSeparated/e.con. +inline "cic:/CoRN/ftc/RefSeparated/e.con". -inline cic:/CoRN/ftc/RefSeparated/RS_He.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_He.con". -inline cic:/CoRN/ftc/RefSeparated/contF'.con. +inline "cic:/CoRN/ftc/RefSeparated/contF'.con". -inline cic:/CoRN/ftc/RefSeparated/d.con. +inline "cic:/CoRN/ftc/RefSeparated/d.con". -inline cic:/CoRN/ftc/RefSeparated/RS_Hd.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_Hd.con". -inline cic:/CoRN/ftc/RefSeparated/RS_Hd'.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_Hd'.con". -inline cic:/CoRN/ftc/RefSeparated/csi.var. +inline "cic:/CoRN/ftc/RefSeparated/csi.var". -inline cic:/CoRN/ftc/RefSeparated/Hcsi.var. +inline "cic:/CoRN/ftc/RefSeparated/Hcsi.var". -inline cic:/CoRN/ftc/RefSeparated/M.con. +inline "cic:/CoRN/ftc/RefSeparated/M.con". -inline cic:/CoRN/ftc/RefSeparated/deltaP.con. +inline "cic:/CoRN/ftc/RefSeparated/deltaP.con". -inline cic:/CoRN/ftc/RefSeparated/deltaR.con. +inline "cic:/CoRN/ftc/RefSeparated/deltaR.con". -inline cic:/CoRN/ftc/RefSeparated/delta.con. +inline "cic:/CoRN/ftc/RefSeparated/delta.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_deltaP.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_deltaP.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_deltaR.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_deltaR.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_csi.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_csi.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_d.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_d.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_pos.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_pos.con". (* UNEXPORTED Section Defining_ai'. *) -inline cic:/CoRN/ftc/RefSeparated/i.var. +inline "cic:/CoRN/ftc/RefSeparated/i.var". -inline cic:/CoRN/ftc/RefSeparated/Hi.var. +inline "cic:/CoRN/ftc/RefSeparated/Hi.var". -inline cic:/CoRN/ftc/RefSeparated/separation_conseq.con. +inline "cic:/CoRN/ftc/RefSeparated/separation_conseq.con". -inline cic:/CoRN/ftc/RefSeparated/pred1.con. +inline "cic:/CoRN/ftc/RefSeparated/pred1.con". -inline cic:/CoRN/ftc/RefSeparated/pred2.con. +inline "cic:/CoRN/ftc/RefSeparated/pred2.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_aux_lemma.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_aux_lemma.con". -inline cic:/CoRN/ftc/RefSeparated/Hi0.var. +inline "cic:/CoRN/ftc/RefSeparated/Hi0.var". -inline cic:/CoRN/ftc/RefSeparated/Hin.var. +inline "cic:/CoRN/ftc/RefSeparated/Hin.var". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_leEq.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_leEq.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_less.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_less.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_ap.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_ap.con". (* UNEXPORTED End Defining_ai'. *) -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_delta.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_delta.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_delta.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_delta.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_mon_i.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_mon_i.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_mon.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_mon.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_wd.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_wd.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_wd.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_wd.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_part.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_part.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_lemma.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_lemma.con". -inline cic:/CoRN/ftc/RefSeparated/g.var. +inline "cic:/CoRN/ftc/RefSeparated/g.var". -inline cic:/CoRN/ftc/RefSeparated/gP.var. +inline "cic:/CoRN/ftc/RefSeparated/gP.var". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_points.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con". (* UNEXPORTED End Separating__Separated.