]> matita.cs.unibo.it Git - helm.git/commit
helm_registry: added the pair unmarshaller
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 17 Nov 2006 18:20:47 +0000 (18:20 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 17 Nov 2006 18:20:47 +0000 (18:20 +0000)
commit876f16ec4e9080bad4e39bd9c203d6529dcf4f56
tree0b151b02054fc00729197162f27184f7e518904d
parentbb691187f8bbe22ec37ca41f9f3f42f9d8e505df
helm_registry: added the pair unmarshaller
grafiteAstPp: bug-fixed
transcript: coercion handling improved
CoRN-Decl: regenerated accordingly
--ehis line, and those below, will be ignored--

M    software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma
M    software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma
M    software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma
M    software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma
M    software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma
M    software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma
M    software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma
M    software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma
M    software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma
M    software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma
M    software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma
M    software/matita/contribs/CoRN-Decl/model/rings/Zring.ma
M    software/matita/contribs/CoRN-Decl/model/rings/Qring.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Zsec.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma
M    software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma
M    software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma
M    software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma
M    software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma
M    software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma
M    software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
M    software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma
M    software/matita/contribs/CoRN-Decl/metrics/Equiv.ma
M    software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
M    software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
M    software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
M    software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
M    software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma
M    software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
M    software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma
M    software/matita/contribs/CoRN-Decl/reals/CReals1.ma
M    software/matita/contribs/CoRN-Decl/reals/Series.ma
M    software/matita/contribs/CoRN-Decl/reals/NRootIR.ma
M    software/matita/contribs/CoRN-Decl/reals/CPoly_Contin.ma
M    software/matita/contribs/CoRN-Decl/reals/IVT.ma
M    software/matita/contribs/CoRN-Decl/reals/RealLists.ma
M    software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma
M    software/matita/contribs/CoRN-Decl/reals/Cauchy_CReals.ma
M    software/matita/contribs/CoRN-Decl/reals/RealFuncts.ma
M    software/matita/contribs/CoRN-Decl/reals/Intervals.ma
M    software/matita/contribs/CoRN-Decl/reals/OddPolyRootIR.ma
M    software/matita/contribs/CoRN-Decl/reals/CReals.ma
M    software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma
M    software/matita/contribs/CoRN-Decl/reals/Q_dense.ma
M    software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma
M    software/matita/contribs/CoRN-Decl/reals/R_morphism.ma
M    software/matita/contribs/CoRN-Decl/reals/CSumsReals.ma
M    software/matita/contribs/CoRN-Decl/reals/Bridges_LUB.ma
M    software/matita/contribs/CoRN-Decl/complex/NRootCC.ma
M    software/matita/contribs/CoRN-Decl/complex/CComplex.ma
M    software/matita/contribs/CoRN-Decl/complex/AbsCC.ma
M    software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma
D    software/matita/contribs/CoRN-Decl/CoRN_notation.ma
M    software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma
M    software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma
M    software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma
M    software/matita/contribs/CoRN-Decl/fta/CC_Props.ma
M    software/matita/contribs/CoRN-Decl/fta/FTAreg.ma
M    software/matita/contribs/CoRN-Decl/fta/FTA.ma
M    software/matita/contribs/CoRN-Decl/fta/MainLemma.ma
M    software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma
M    software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma
M    software/matita/contribs/CoRN-Decl/tactics/DiffTactics1.ma
M    software/matita/contribs/CoRN-Decl/tactics/DiffTactics2.ma
M    software/matita/contribs/CoRN-Decl/tactics/DiffTactics3.ma
M    software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
M    software/matita/contribs/CoRN-Decl/tactics/Opaque_algebra.ma
M    software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
M    software/matita/contribs/CoRN-Decl/tactics/Step.ma
M    software/matita/contribs/CoRN-Decl/tactics/AlgReflection.ma
M    software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma
M    software/matita/contribs/CoRN-Decl/tactics/Transparent_algebra.ma
M    software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
M    software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma
M    software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
M    software/matita/contribs/CoRN-Decl/transc/Exponential.ma
M    software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
M    software/matita/contribs/CoRN-Decl/transc/Pi.ma
M    software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma
M    software/matita/contribs/CoRN-Decl/transc/SinCos.ma
M    software/matita/contribs/CoRN-Decl/transc/TrigMon.ma
M    software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma
M    software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma
M    software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma
M    software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma
M    software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma
M    software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
M    software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma
M    software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma
M    software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma
M    software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma
M    software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma
M    software/matita/contribs/CoRN-Decl/ftc/Partitions.ma
M    software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma
M    software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma
M    software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma
M    software/matita/contribs/CoRN-Decl/ftc/Derivative.ma
M    software/matita/contribs/CoRN-Decl/ftc/Composition.ma
M    software/matita/contribs/CoRN-Decl/ftc/Integral.ma
M    software/matita/contribs/CoRN-Decl/ftc/Continuity.ma
M    software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma
M    software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma
M    software/matita/contribs/CoRN-Decl/ftc/Taylor.ma
M    software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma
M    software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma
M    software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
M    software/matita/contribs/CoRN-Decl/ftc/FTC.ma
M    software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma
M    software/matita/contribs/CoRN-Decl/ftc/Rolle.ma
M    software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma
M    software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
M    software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma
M    software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma
M    software/matita/contribs/CoRN-Decl/algebra/CRings.ma
M    software/matita/contribs/CoRN-Decl/algebra/Expon.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSums.ma
M    software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
M    software/matita/contribs/CoRN-Decl/algebra/CLogic.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
M    software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
M    software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma
M    software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma
M    software/matita/contribs/CoRN-Decl/algebra/Basics.ma
M    software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma
M    software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma
M    software/matita/contribs/CoRN-Decl/algebra/CFields.ma
M    software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma
M    software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma
M    software/matita/contribs/CoRN-Decl/algebra/ListType.ma
M    software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma
M    software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma
M    software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma
M    software/matita/contribs/CoRN-Decl/algebra/CGroups.ma
A    software/matita/contribs/CoRN-Decl/CoRN.ma
M    software/components/grafite/grafiteAstPp.ml
M    software/components/binaries/transcript/CoRN.conf.xml
M    software/components/binaries/transcript/grafite.ml
M    software/components/binaries/transcript/v8Parser.mly
M    software/components/binaries/transcript/types.ml
M    software/components/binaries/transcript/engine.ml
M    software/components/registry/helm_registry.ml
M    software/components/registry/helm_registry.mli
166 files changed:
helm/software/components/binaries/transcript/CoRN.conf.xml
helm/software/components/binaries/transcript/engine.ml
helm/software/components/binaries/transcript/grafite.ml
helm/software/components/binaries/transcript/types.ml
helm/software/components/binaries/transcript/v8Parser.mly
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/registry/helm_registry.ml
helm/software/components/registry/helm_registry.mli
helm/software/matita/contribs/CoRN-Decl/CoRN.ma [new file with mode: 0644]
helm/software/matita/contribs/CoRN-Decl/CoRN_notation.ma [deleted file]
helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma
helm/software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma
helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma
helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma
helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma
helm/software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma
helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma
helm/software/matita/contribs/CoRN-Decl/algebra/Expon.ma
helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma
helm/software/matita/contribs/CoRN-Decl/complex/AbsCC.ma
helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma
helm/software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma
helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma
helm/software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma
helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma
helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma
helm/software/matita/contribs/CoRN-Decl/fta/CC_Props.ma
helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma
helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma
helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma
helm/software/matita/contribs/CoRN-Decl/fta/FTA.ma
helm/software/matita/contribs/CoRN-Decl/fta/FTAreg.ma
helm/software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma
helm/software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma
helm/software/matita/contribs/CoRN-Decl/fta/MainLemma.ma
helm/software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma
helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
helm/software/matita/contribs/CoRN-Decl/ftc/Composition.ma
helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma
helm/software/matita/contribs/CoRN-Decl/ftc/Derivative.ma
helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma
helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma
helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma
helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma
helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma
helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma
helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma
helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma
helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma
helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma
helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma
helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma
helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma
helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
helm/software/matita/contribs/CoRN-Decl/ftc/Partitions.ma
helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma
helm/software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma
helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma
helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma
helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma
helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma
helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma
helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma
helm/software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma
helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
helm/software/matita/contribs/CoRN-Decl/metrics/Equiv.ma
helm/software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma
helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
helm/software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma
helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma
helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma
helm/software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma
helm/software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma
helm/software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma
helm/software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma
helm/software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma
helm/software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma
helm/software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma
helm/software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma
helm/software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma
helm/software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma
helm/software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma
helm/software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma
helm/software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma
helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma
helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma
helm/software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma
helm/software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma
helm/software/matita/contribs/CoRN-Decl/model/rings/Qring.ma
helm/software/matita/contribs/CoRN-Decl/model/rings/Zring.ma
helm/software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma
helm/software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma
helm/software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma
helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma
helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma
helm/software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma
helm/software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma
helm/software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma
helm/software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma
helm/software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma
helm/software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma
helm/software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma
helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma
helm/software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma
helm/software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma
helm/software/matita/contribs/CoRN-Decl/model/structures/Zsec.ma
helm/software/matita/contribs/CoRN-Decl/reals/Bridges_LUB.ma
helm/software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma
helm/software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma
helm/software/matita/contribs/CoRN-Decl/reals/CPoly_Contin.ma
helm/software/matita/contribs/CoRN-Decl/reals/CReals.ma
helm/software/matita/contribs/CoRN-Decl/reals/CReals1.ma
helm/software/matita/contribs/CoRN-Decl/reals/CSumsReals.ma
helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
helm/software/matita/contribs/CoRN-Decl/reals/Cauchy_CReals.ma
helm/software/matita/contribs/CoRN-Decl/reals/IVT.ma
helm/software/matita/contribs/CoRN-Decl/reals/Intervals.ma
helm/software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma
helm/software/matita/contribs/CoRN-Decl/reals/NRootIR.ma
helm/software/matita/contribs/CoRN-Decl/reals/OddPolyRootIR.ma
helm/software/matita/contribs/CoRN-Decl/reals/Q_dense.ma
helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma
helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma
helm/software/matita/contribs/CoRN-Decl/reals/RealFuncts.ma
helm/software/matita/contribs/CoRN-Decl/reals/RealLists.ma
helm/software/matita/contribs/CoRN-Decl/reals/Series.ma
helm/software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma
helm/software/matita/contribs/CoRN-Decl/tactics/AlgReflection.ma
helm/software/matita/contribs/CoRN-Decl/tactics/DiffTactics1.ma
helm/software/matita/contribs/CoRN-Decl/tactics/DiffTactics2.ma
helm/software/matita/contribs/CoRN-Decl/tactics/DiffTactics3.ma
helm/software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma
helm/software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
helm/software/matita/contribs/CoRN-Decl/tactics/Opaque_algebra.ma
helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
helm/software/matita/contribs/CoRN-Decl/tactics/Step.ma
helm/software/matita/contribs/CoRN-Decl/tactics/Transparent_algebra.ma
helm/software/matita/contribs/CoRN-Decl/transc/Exponential.ma
helm/software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma
helm/software/matita/contribs/CoRN-Decl/transc/Pi.ma
helm/software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma
helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma
helm/software/matita/contribs/CoRN-Decl/transc/TrigMon.ma
helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma