@echo -n
opt: transcript.opt $(EXTRAS) .depend.opt
- #echo -n
+ @echo -n
-transcript: $(CMIS) $(CMOS) $(EXTRAS) $(LIBRARIES)
+transcript: $(CMIS) $(CMOS) $(EXTRAS)
@echo " OCAMLC $(CMOS)"
$(H)$(OCAMLC) -o $@ $(CMOS)
-transcript.opt: $(CMIS) $(CMXS) $(EXTRAS) $(LIBRARIES_OPT)
+transcript.opt: $(CMIS) $(CMXS) $(EXTRAS)
@echo " OCAMLOPT $(CMXS)"
$(H)$(OCAMLOPT) -o $@ $(CMXS)
depend.opt: .depend.opt
-%.cmi: %.mli $(EXTRAS)
+%.cmi: %.mli $(EXTRAS)
@echo " OCAMLC $<"
$(H)$(OCAMLC) -c $<
-%.cmo %.cmi: %.ml $(EXTRAS)
+%.cmo %.cmi: %.ml $(EXTRAS) $(LIBRARIES)
@echo " OCAMLC $<"
$(H)$(OCAMLC) -c $<
-%.cmx: %.ml $(EXTRAS)
+%.cmx: %.ml $(EXTRAS) $(LIBRARIES_OPT)
@echo " OCAMLOPT $<"
$(H)$(OCAMLOPT) -c $<
%.ml %.mli: %.mly $(EXTRAS)
let baseuri = Filename.concat st.output_base_uri name in
set_items st name [T.BaseUri baseuri]
-let require st name =
- set_items st name [T.Include st.package]
+let require st name inc =
+ set_items st name [T.Include inc]
let commit st name =
let i = get_index st name in
st.scripts.(i) <- default_script
let produce st =
+ let notation = st.package ^ "_notation" in
let init name = set_heading st name; set_baseuri st name in
let partition = function
| T.Notation _ -> false
let local_items, global_items = List.partition partition items in
let comment = T.Line (Printf.sprintf "From %s" name) in
if global_items <> [] then
- set_items st st.package (comment :: global_items);
- init name; require st name;
+ set_items st notation (comment :: global_items);
+ init name; require st name notation;
set_items st name local_items; commit st name
with e ->
prerr_endline (Printexc.to_string e); close_in ich
in
- init st.package; List.iter (produce st) st.files; commit st st.package
+ init notation; List.iter (produce st) st.files; commit st notation
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/CoRN-Decl/CoRN".
-
-(* From algebra/Basics ****************************************************)
-
-(* NOTATION
-Notation Pair := (pair (B:=_)).
-*)
-
-(* NOTATION
-Notation Proj1 := (proj1 (B:=_)).
-*)
-
-(* NOTATION
-Notation Proj2 := (proj2 (B:=_)).
-*)
-
-(* From algebra/CFields ***************************************************)
-
-(* NOTATION
-Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
-*)
-
-(* NOTATION
-Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
-*)
-
-(* NOTATION
-Infix "{/}" := Fdiv (at level 41, no associativity).
-*)
-
-(* From algebra/CGroups ***************************************************)
-
-(* NOTATION
-Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
-*)
-
-(* NOTATION
-Infix "[-]" := cg_minus (at level 50, left associativity).
-*)
-
-(* NOTATION
-Notation "{--} x" := (Finv x) (at level 2, right associativity).
-*)
-
-(* NOTATION
-Infix "{-}" := Fminus (at level 50, left associativity).
-*)
-
-(* From algebra/CLogic ****************************************************)
-
-(* NOTATION
-Infix "IFF" := Iff (at level 60, right associativity).
-*)
-
-(* NOTATION
-Infix "or" := COr (at level 85, right associativity).
-*)
-
-(* NOTATION
-Infix "and" := CAnd (at level 80, right associativity).
-*)
-
-(* NOTATION
-Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp)
- (at level 0, x at level 99) : type_scope.
-*)
-
-(* NOTATION
-Notation "{ x : A | P | Q }" :=
- (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
- type_scope.
-*)
-
-(* NOTATION
-Notation ProjT1 := (proj1_sigT _ _).
-*)
-
-(* NOTATION
-Notation ProjT2 := (proj2_sigT _ _).
-*)
-
-(* From algebra/CMonoids **************************************************)
-
-(* NOTATION
-Notation Zero := (cm_unit _).
-*)
-
-(* From algebra/COrdAbs ***************************************************)
-
-(* NOTATION
-Notation ZeroR := (Zero:R).
-*)
-
-(* NOTATION
-Notation AbsBig := (absBig _).
-*)
-
-(* From algebra/COrdFields ************************************************)
-
-(* NOTATION
-Infix "[<]" := cof_less (at level 70, no associativity).
-*)
-
-(* NOTATION
-Infix "[>]" := greater (at level 70, no associativity).
-*)
-
-(* NOTATION
-Infix "[<=]" := leEq (at level 70, no associativity).
-*)
-
-(* NOTATION
-Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
-*)
-
-(* NOTATION
-Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
-*)
-
-(* From algebra/COrdFields2 ***********************************************)
-
-(* NOTATION
-Notation ZeroR := (Zero:R).
-*)
-
-(* NOTATION
-Notation OneR := (One:R).
-*)
-
-(* From algebra/CPoly_ApZero **********************************************)
-
-(* NOTATION
-Notation RX := (cpoly_cring R).
-*)
-
-(* NOTATION
-Notation RX := (cpoly_cring R).
-*)
-
-(* NOTATION
-Notation RX := (cpoly_cring R).
-*)
-
-(* From algebra/CPoly_Degree **********************************************)
-
-(* NOTATION
-Notation RX := (cpoly_cring R).
-*)
-
-(* NOTATION
-Notation RX := (cpoly_cring R).
-*)
-
-(* NOTATION
-Notation FX := (cpoly_cring F).
-*)
-
-(* From algebra/CPoly_NthCoeff ********************************************)
-
-(* NOTATION
-Notation RX := (cpoly_cring R).
-*)
-
-(* NOTATION
-Notation RX := (cpoly_cring R).
-*)
-
-(* From algebra/CPolynomials **********************************************)
-
-(* NOTATION
-Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity).
-*)
-
-(* NOTATION
-Notation RX := (cpoly_cring CR).
-*)
-
-(* NOTATION
-Infix "!" := cpoly_apply_fun (at level 1, no associativity).
-*)
-
-(* NOTATION
-Notation RX := (cpoly_cring R).
-*)
-
-(* NOTATION
-Notation Cpoly := (cpoly CR).
-*)
-
-(* NOTATION
-Notation Cpoly_zero := (cpoly_zero CR).
-*)
-
-(* NOTATION
-Notation Cpoly_linear := (cpoly_linear CR).
-*)
-
-(* NOTATION
-Notation Cpoly_cring := (cpoly_cring CR).
-*)
-
-(* From algebra/CRings ****************************************************)
-
-(* NOTATION
-Notation One := (cr_one _).
-*)
-
-(* NOTATION
-Infix "[*]" := cr_mult (at level 40, left associativity).
-*)
-
-(* NOTATION
-Notation "x [^] n" := (nexp_op _ n x) (at level 20).
-*)
-
-(* NOTATION
-Notation Two := (nring 2).
-*)
-
-(* NOTATION
-Notation Three := (nring 3).
-*)
-
-(* NOTATION
-Notation Four := (nring 4).
-*)
-
-(* NOTATION
-Notation Six := (nring 6).
-*)
-
-(* NOTATION
-Notation Eight := (nring 8).
-*)
-
-(* NOTATION
-Notation Twelve := (nring 12).
-*)
-
-(* NOTATION
-Notation Sixteen := (nring 16).
-*)
-
-(* NOTATION
-Notation Nine := (nring 9).
-*)
-
-(* NOTATION
-Notation Eighteen := (nring 18).
-*)
-
-(* NOTATION
-Notation TwentyFour := (nring 24).
-*)
-
-(* NOTATION
-Notation FortyEight := (nring 48).
-*)
-
-(* NOTATION
-Infix "{*}" := Fmult (at level 40, left associativity).
-*)
-
-(* NOTATION
-Infix "{**}" := Fscalmult (at level 40, left associativity).
-*)
-
-(* NOTATION
-Infix "{^}" := Fnth (at level 30, right associativity).
-*)
-
-(* From algebra/CSemiGroups ***********************************************)
-
-(* NOTATION
-Infix "[+]" := csg_op (at level 50, left associativity).
-*)
-
-(* NOTATION
-Infix "{+}" := Fplus (at level 50, left associativity).
-*)
-
-(* From algebra/CSetoidFun ************************************************)
-
-(* NOTATION
-Notation Conj := (conjP _).
-*)
-
-(* NOTATION
-Notation BDom := (bpfdom _ _).
-*)
-
-(* NOTATION
-Notation Dom := (pfdom _).
-*)
-
-(* NOTATION
-Notation Part := (pfpfun _).
-*)
-
-(* NOTATION
-Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
-*)
-
-(* NOTATION
-Notation FId := (Fid _).
-*)
-
-(* NOTATION
-Infix "[o]" := Fcomp (at level 65, no associativity).
-*)
-
-(* NOTATION
-Notation Prj1 := (prj1 _ _ _ _).
-*)
-
-(* NOTATION
-Notation Prj2 := (prj2 _ _ _ _).
-*)
-
-(* From algebra/CSetoids **************************************************)
-
-(* NOTATION
-Infix "[=]" := cs_eq (at level 70, no associativity).
-*)
-
-(* NOTATION
-Infix "[#]" := cs_ap (at level 70, no associativity).
-*)
-
-(* NOTATION
-Infix "[~=]" := cs_neq (at level 70, no associativity).
-*)
-
-(* From algebra/CVectorSpace **********************************************)
-
-(* NOTATION
-Infix "[']" := vs_op (at level 30, no associativity).
-*)
-
-(* From algebra/Expon *****************************************************)
-
-(* NOTATION
-Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0).
-*)
-
-(* From complex/CComplex **************************************************)
-
-(* NOTATION
-Notation CCX := (cpoly_cring CC).
-*)
-
-(* NOTATION
-Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
-*)
-
-(* From ftc/FTC ***********************************************************)
-
-(* NOTATION
-Notation "[-S-] F" := (Fprim F) (at level 20).
-*)
-
-(* From ftc/Integral ******************************************************)
-
-(* NOTATION
-Notation Integral := (integral _ _ Hab).
-*)
-
-(* From ftc/RefLemma ******************************************************)
-
-(* NOTATION
-Notation g := RL_g.
-*)
-
-(* NOTATION
-Notation h := RL_h.
-*)
-
-(* NOTATION
-Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
-*)
-
-(* NOTATION
-Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
-*)
-
-(* NOTATION
-Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
-*)
-
-(* From ftc/RefSeparated **************************************************)
-
-(* NOTATION
-Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
-*)
-
-(* NOTATION
-Notation just2 :=
- (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)).
-*)
-
-(* From ftc/RefSeparating *************************************************)
-
-(* NOTATION
-Notation m := RS'_m.
-*)
-
-(* NOTATION
-Notation h := RS'_h.
-*)
-
-(* NOTATION
-Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
-*)
-
-(* NOTATION
-Notation just2 :=
- (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)).
-*)
-
-(* From ftc/Rolle *********************************************************)
-
-(* NOTATION
-Notation cp := (compact_part a b Hab' d Hd).
-*)
-
-(* From ftc/TaylorLemma ***************************************************)
-
-(* NOTATION
-Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
-*)
-
-(* NOTATION
-Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
-*)
-
-(* From ftc/WeakIVT *******************************************************)
-
-(* NOTATION
-Infix "**" := prodT (at level 20).
-*)
-
-(* From metrics/CPseudoMSpaces ********************************************)
-
-(* NOTATION
-Infix "[-d]" := cms_d (at level 68, left associativity).
-*)
-
-(* From model/structures/Nsec *********************************************)
-
-(* NOTATION
-Infix "{#N}" := ap_nat (no associativity, at level 90).
-*)
-
-(* From model/structures/Qsec *********************************************)
-
-(* NOTATION
-Infix "{=Q}" := Qeq (no associativity, at level 90).
-*)
-
-(* NOTATION
-Infix "{#Q}" := Qap (no associativity, at level 90).
-*)
-
-(* NOTATION
-Infix "{<Q}" := Qlt (no associativity, at level 90).
-*)
-
-(* NOTATION
-Infix "{+Q}" := Qplus (no associativity, at level 85).
-*)
-
-(* NOTATION
-Infix "{*Q}" := Qmult (no associativity, at level 80).
-*)
-
-(* NOTATION
-Notation "{-Q}" := Qopp (at level 1, left associativity).
-*)
-
-(* From model/structures/Zsec *********************************************)
-
-(* NOTATION
-Infix "{#Z}" := ap_Z (no associativity, at level 90).
-*)
-
-(* From reals/Bridges_LUB *************************************************)
-
-(* NOTATION
-Notation "( p , q )" := (pairT p q).
-*)
-
-(* From reals/CMetricFields ***********************************************)
-
-(* NOTATION
-Notation MAbs := (cmf_abs _).
-*)
-
-(* From reals/CauchySeq ***************************************************)
-
-(* NOTATION
-Notation PartIR := (PartFunct IR).
-*)
-
-(* NOTATION
-Notation ProjIR1 := (prj1 IR _ _ _).
-*)
-
-(* NOTATION
-Notation ProjIR2 := (prj2 IR _ _ _).
-*)
-
-(* NOTATION
-Notation ZeroR := (Zero:IR).
-*)
-
-(* NOTATION
-Notation OneR := (One:IR).
-*)
-
-(* From reals/Cauchy_CReals ***********************************************)
-
-(* NOTATION
-Notation "'R_COrdField''" := (R_COrdField F).
-*)
-
-(* From reals/Intervals ***************************************************)
-
-(* NOTATION
-Notation Compact := (compact _ _).
-*)
-
-(* NOTATION
-Notation FRestr := (Frestr (compact_wd _ _ _)).
-*)
-
-(* From reals/Q_dense *****************************************************)
-
-(* NOTATION
-Notation "( A , B )" := (pairT A B).
-*)
-
-(* From tactics/FieldReflection *******************************************)
-
-(* NOTATION
-Notation II := (interpF F val unop binop pfun).
-*)
-
-(* From tactics/GroupReflection *******************************************)
-
-(* NOTATION
-Notation II := (interpG G val unop binop pfun).
-*)
-
-(* From tactics/RingReflection ********************************************)
-
-(* NOTATION
-Notation II := (interpR R val unop binop pfun).
-*)
-
-(* From transc/RealPowers *************************************************)
-
-(* NOTATION
-Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
-*)
-
-(* NOTATION
-Notation "F {!} G" := (FPower F G) (at level 20).
-*)
-
set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CAbGroups".
-include "CoRN.ma".
+include "CoRN_notation.ma".
include "algebra/CGroups.ma".
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CAbMonoids".
-include "CoRN.ma".
+include "CoRN_notation.ma".
include "algebra/CMonoids.ma".
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CFields".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CFields.v,v 1.12 2004/04/23 10:00:52 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CGroups".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CGroups.v,v 1.9 2004/04/23 10:00:52 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CLogic".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CLogic.v,v 1.10 2004/04/09 15:58:31 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CMonoids".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CMonoids.v,v 1.3 2004/04/07 15:07:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdAbs".
-include "CoRN.ma".
+include "CoRN_notation.ma".
include "algebra/COrdFields2.ma".
set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdCauchy".
-include "CoRN.ma".
+include "CoRN_notation.ma".
include "algebra/COrdAbs.ma".
set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: COrdFields.v,v 1.6 2004/04/23 10:00:52 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields2".
-include "CoRN.ma".
+include "CoRN_notation.ma".
include "algebra/COrdFields.ma".
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_ApZero".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPoly_ApZero.v,v 1.3 2004/04/23 10:00:53 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_Degree".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPoly_Degree.v,v 1.5 2004/04/23 10:00:53 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_NthCoeff".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPoly_NthCoeff.v,v 1.6 2004/04/23 10:00:53 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPolynomials".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPolynomials.v,v 1.9 2004/04/23 10:00:53 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CRings".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CRings.v,v 1.8 2004/04/23 10:00:53 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSemiGroups".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CSemiGroups.v,v 1.8 2004/04/22 14:49:43 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoidFun".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoidInc".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CSetoidInc.v,v 1.3 2004/04/22 14:49:43 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoids".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id.v,v 1.18 2002/11/25 14:43:42 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CVectorSpace".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CVectorSpace.v,v 1.4 2004/04/23 10:00:54 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/Cauchy_COF".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/Expon".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Expon.v,v 1.5 2004/04/23 10:00:54 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/ListType".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/complex/AbsCC".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: AbsCC.v,v 1.2 2004/04/23 10:00:54 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/complex/CComplex".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CComplex.v,v 1.8 2004/04/23 10:00:55 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/complex/Complex_Exponential".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Complex_Exponential.v,v 1.4 2004/04/23 10:00:55 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/complex/NRootCC".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: NRootCC.v,v 1.9 2004/04/23 10:00:55 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/IDA/Ch6".
-include "CoRN.ma".
+include "CoRN_notation.ma".
include "algebra/CSemiGroups.ma".
set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/per/csetfun".
-include "CoRN.ma".
+include "CoRN_notation.ma".
include "algebra/CSetoids.ma".
set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun".
-include "CoRN.ma".
+include "CoRN_notation.ma".
inline "cic:/CoRN/devel/loeb/per/lst2fun/F'.con".
set "baseuri" "cic:/matita/CoRN-Decl/fta/CC_Props".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CC_Props.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/fta/CPoly_Contin1".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPoly_Contin1.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/fta/CPoly_Rev".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPoly_Rev.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/fta/CPoly_Shift".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPoly_Shift.v,v 1.4 2004/04/23 10:00:56 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/fta/FTA".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: FTA.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/fta/FTAreg".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: FTAreg.v,v 1.4 2004/04/23 10:00:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/fta/KeyLemma".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: KeyLemma.v,v 1.5 2004/04/23 10:00:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/fta/KneserLemma".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: KneserLemma.v,v 1.7 2004/04/23 10:00:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/fta/MainLemma".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: MainLemma.v,v 1.3 2004/04/23 10:00:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/COrdLemmas".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: COrdLemmas.v,v 1.2 2004/04/23 10:00:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/CalculusTheorems".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CalculusTheorems.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Composition".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Continuity".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Continuity.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Derivative".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Derivative.v,v 1.7 2004/04/23 10:00:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/DerivativeOps".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: DerivativeOps.v,v 1.3 2004/04/23 10:00:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Differentiability".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/FTC".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: FTC.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSequence".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: FunctSequence.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSeries".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: FunctSeries.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSums".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: FunctSums.v,v 1.5 2004/04/23 10:00:59 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Integral".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Integral.v,v 1.10 2004/04/23 10:00:59 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/IntervalFunct".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: IntervalFunct.v,v 1.5 2004/04/08 15:28:06 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreFunSeries".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreFunctions".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntegrals".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: MoreIntegrals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntervals".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: MoreIntervals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/NthDerivative".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: NthDerivative.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartFunEquality".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: PartFunEquality.v,v 1.8 2004/04/23 10:00:59 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartInterval".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Partitions".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Partitions.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefLemma".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: RefLemma.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSepRef".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: RefSepRef.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSeparated".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: RefSeparated.v,v 1.8 2004/04/23 10:01:00 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSeparating".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: RefSeparating.v,v 1.7 2004/04/23 10:01:01 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Rolle".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Rolle.v,v 1.6 2004/04/23 10:01:01 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/StrongIVT".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: StrongIVT.v,v 1.5 2004/04/23 10:01:01 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Taylor".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Taylor.v,v 1.10 2004/04/23 10:01:01 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/TaylorLemma".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/ftc/WeakIVT".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: WeakIVT.v,v 1.9 2004/04/23 10:01:01 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/metrics/CMetricSpaces".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPMSTheory".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPseudoMSpaces.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/metrics/ContFunctions".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: ContFunctions.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/metrics/Equiv".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Equiv.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/metrics/IR_CPMSpace".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: IR_CPMSpace.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/metrics/Prod_Sub".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Prod_Sub.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/QSposabgroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: QSposabgroup.v,v 1.5 2004/04/08 08:20:31 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/Qabgroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qabgroup.v,v 1.5 2004/04/08 08:20:31 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/Qposabgroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qposabgroup.v,v 1.6 2004/04/08 08:20:31 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/Zabgroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Zabgroup.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/fields/Qfield".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qfield.v,v 1.8 2004/04/08 08:20:32 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/groups/QSposgroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: QSposgroup.v,v 1.6 2004/04/08 08:20:32 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/groups/Qgroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qgroup.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/groups/Qposgroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qposgroup.v,v 1.6 2004/04/08 08:20:32 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/groups/Zgroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Zgroup.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Nmonoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Nmonoid.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Nposmonoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Nposmonoid.v,v 1.6 2004/04/08 08:20:33 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/QSposmonoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: QSposmonoid.v,v 1.5 2004/04/08 08:20:33 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Qmonoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qmonoid.v,v 1.7 2004/04/08 08:20:33 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Qposmonoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qposmonoid.v,v 1.7 2004/04/08 08:20:33 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Zmonoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Zmonoid.v,v 1.6 2004/04/08 08:20:33 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/non_examples/N_no_group".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: N_no_group.v,v 1.5 2004/04/08 08:20:33 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/non_examples/Npos_no_group".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Npos_no_group.v,v 1.6 2004/04/08 08:20:33 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/non_examples/Npos_no_monoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Npos_no_monoid.v,v 1.5 2004/04/08 08:20:34 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/ordfields/Qordfield".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qordfield.v,v 1.9 2004/04/23 10:01:03 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/reals/Cauchy_IR".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Cauchy_IR.v,v 1.2 2004/04/06 15:46:03 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/rings/Qring".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qring.v,v 1.8 2004/04/23 10:01:03 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/rings/Zring".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Zring.v,v 1.6 2004/04/08 08:20:34 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Npossemigroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Npossemigroup.v,v 1.6 2004/04/08 08:20:34 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Nsemigroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Nsemigroup.v,v 1.6 2004/04/08 08:20:34 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/QSpossemigroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: QSpossemigroup.v,v 1.5 2004/04/08 08:20:35 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Qpossemigroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qpossemigroup.v,v 1.6 2004/04/08 08:20:35 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Qsemigroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qsemigroup.v,v 1.6 2004/04/08 08:20:35 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Zsemigroup".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Zsemigroup.v,v 1.6 2004/04/08 08:20:35 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Npossetoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Npossetoid.v,v 1.3 2004/04/06 15:46:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Nsetoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Nsetoid.v,v 1.4 2004/04/06 15:46:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Qpossetoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qpossetoid.v,v 1.4 2004/04/06 15:46:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Qsetoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qsetoid.v,v 1.6 2004/04/06 15:46:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Zsetoid".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Zsetoid.v,v 1.5 2004/04/07 15:08:08 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Npossec".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Npossec.v,v 1.3 2004/04/06 15:46:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Nsec".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Nsec.v,v 1.6 2004/04/06 15:46:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Qpossec".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qpossec.v,v 1.5 2004/04/06 15:46:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Qsec".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Qsec.v,v 1.7 2004/04/08 08:20:35 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Zsec".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Zsec.v,v 1.5 2004/04/06 15:46:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Bridges_LUB".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Bridges_iso".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CMetricFields".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CMetricFields.v,v 1.6 2004/04/23 10:01:03 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CPoly_Contin".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CPoly_Contin.v,v 1.6 2004/04/23 10:01:03 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CReals".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CReals.v,v 1.2 2004/04/05 11:35:38 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CReals1".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CReals1.v,v 1.4 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CSumsReals".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CSumsReals.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CauchySeq".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: CauchySeq.v,v 1.8 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Cauchy_CReals".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Cauchy_CReals.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/IVT".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: IVT.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Intervals".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Intervals.v,v 1.10 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Max_AbsIR".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Max_AbsIR.v,v 1.13 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/NRootIR".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: NRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/OddPolyRootIR".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: OddPolyRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Q_dense".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Q_in_CReals".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Q_in_CReals.v,v 1.10 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/R_morphism".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/RealFuncts".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: RealFuncts.v,v 1.4 2004/04/07 15:08:10 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/RealLists".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: RealLists.v,v 1.4 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Series".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Series.v,v 1.6 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/iso_CReals".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/AlgReflection".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: AlgReflection.v,v 1.2 2004/03/26 16:07:03 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/DiffTactics1".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/DiffTactics2".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: DiffTactics2.v,v 1.1.1.1 2004/02/05 16:25:45 lionelm Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/DiffTactics3".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: DiffTactics3.v,v 1.1.1.1 2004/02/05 16:25:44 lionelm Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/FieldReflection".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: FieldReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/GroupReflection".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: GroupReflection.v,v 1.3 2004/04/23 10:01:06 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/Opaque_algebra".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Opaque_algebra.v,v 1.1 2004/02/11 10:56:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/RingReflection".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: RingReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/Step".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/Transparent_algebra".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Transparent_algebra.v,v 1.1 2004/02/11 10:56:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/Exponential".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Exponential.v,v 1.7 2004/04/23 10:01:07 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/InvTrigonom".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: InvTrigonom.v,v 1.9 2004/04/23 10:01:07 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/Pi".
-include "CoRN.ma".
+include "CoRN_notation.ma".
include "transc/SinCos.ma".
set "baseuri" "cic:/matita/CoRN-Decl/transc/PowerSeries".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: PowerSeries.v,v 1.8 2004/04/23 10:01:08 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/RealPowers".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: RealPowers.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/SinCos".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: SinCos.v,v 1.6 2004/04/23 10:01:08 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/TaylorSeries".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: TaylorSeries.v,v 1.7 2004/04/23 10:01:08 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/TrigMon".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: TrigMon.v,v 1.9 2004/04/23 10:01:08 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/Trigonometric".
-include "CoRN.ma".
+include "CoRN_notation.ma".
(* $Id: Trigonometric.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
projects / helm.git / commitdiff