]> matita.cs.unibo.it Git - helm.git/commit
new CoRN development, generated by transcript
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 15 Nov 2006 19:52:45 +0000 (19:52 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 15 Nov 2006 19:52:45 +0000 (19:52 +0000)
commit0e0d5c57eb154bf20d101f09e560401434156c1d
tree60bb4a2182a2ac148a708ddebf4210f267546597
parentad17757edcc6cf75be576268fab8cf52751d679a
new CoRN development, generated by transcript
158 files changed:
matita/contribs/CoRN-Decl/CoRN.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/Basics.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CAbGroups.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CFields.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CGroups.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CLogic.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CMonoids.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/COrdAbs.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/COrdFields.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/COrdFields2.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CPolynomials.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CRings.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSetoids.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSums.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/Expon.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/ListType.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/complex/AbsCC.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/complex/CComplex.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/complex/NRootCC.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/CC_Props.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/FTA.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/FTAreg.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/KeyLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/KneserLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/MainLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Composition.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Continuity.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Derivative.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Differentiability.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/FTC.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/FunctSequence.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/FunctSeries.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/FunctSums.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Integral.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/NthDerivative.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/PartInterval.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Partitions.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/RefLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/RefSepRef.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/RefSeparated.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/RefSeparating.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Rolle.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/StrongIVT.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Taylor.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/WeakIVT.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/makefile [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/ContFunctions.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/Equiv.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/fields/Qfield.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/groups/Qgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/groups/Zgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/rings/Qring.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/rings/Zring.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Npossec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Nsec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Qpossec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Qsec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Zsec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Bridges_LUB.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Bridges_iso.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CMetricFields.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CPoly_Contin.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CReals1.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CSumsReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CauchySeq.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Cauchy_CReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/IVT.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Intervals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/NRootIR.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/OddPolyRootIR.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Q_dense.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/R_morphism.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/RealFuncts.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/RealLists.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Series.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/iso_CReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/AlgReflection.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/DiffTactics1.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/DiffTactics2.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/DiffTactics3.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/FieldReflection.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/GroupReflection.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/Opaque_algebra.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/RingReflection.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/Step.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/Transparent_algebra.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/Exponential.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/InvTrigonom.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/Pi.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/PowerSeries.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/RealPowers.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/SinCos.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/TaylorSeries.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/TrigMon.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/Trigonometric.ma [new file with mode: 0644]