]> matita.cs.unibo.it Git - helm.git/commit - helm/software/matita/contribs/procedural/Coq/Num/SubProps.mma
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1fb0f39) | patch
transcript: we improved the parser/lexer to read the scripts of the standard
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 4 Sep 2008 16:08:25 +0000 (16:08 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 4 Sep 2008 16:08:25 +0000 (16:08 +0000)
commit29714797b01e0ac8c22e4df2827b1785a759f482
tree3f2bb675febc9decee83938f0fd4cfdb5b42c589tree | snapshot
parent1fb0f39de8b87920d2f15f9e33929d372fa518ddcommit | diff
transcript: we improved the parser/lexer to read the scripts of the standard
            library of coq. Coercion extraction is disabled for now.
contribs/procedural: new root for mma files generated by transcript.
                     We now have the mma files of the cic:/Coq/* objects
394 files changed:
helm/software/components/binaries/transcript/v8Lexer.mll diff | blob | history
helm/software/components/binaries/transcript/v8Parser.mly diff | blob | history
helm/software/matita/contribs/procedural/CoRN/CoRN.conf.xml [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/CoRN.ma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/Makefile [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/Basics.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CAbGroups.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CAbMonoids.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CFields.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CGroups.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CLogic.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CMonoids.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/COrdAbs.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/COrdCauchy.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/COrdFields.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/COrdFields2.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CPoly_ApZero.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CPoly_Degree.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CPoly_NthCoeff.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CPolynomials.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CRings.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CSemiGroups.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CSetoidFun.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CSetoidInc.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CSetoids.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CSums.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/CVectorSpace.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/Cauchy_COF.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/Expon.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/algebra/ListType.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/complex/AbsCC.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/complex/CComplex.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/complex/Complex_Exponential.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/complex/NRootCC.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/depends [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/devel/loeb/IDA/Ch6.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/devel/loeb/per/csetfun.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/devel/loeb/per/lst2fun.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/CC_Props.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/CPoly_Contin1.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/CPoly_Rev.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/CPoly_Shift.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/FTA.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/FTAreg.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/KeyLemma.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/KneserLemma.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/fta/MainLemma.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/COrdLemmas.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/CalculusTheorems.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/Composition.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/Continuity.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/Derivative.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/DerivativeOps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/Differentiability.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/FTC.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/FunctSequence.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/FunctSeries.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/FunctSums.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/Integral.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/IntervalFunct.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/MoreFunSeries.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/MoreFunctions.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/MoreIntegrals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/MoreIntervals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/NthDerivative.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/PartFunEquality.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/PartInterval.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/Partitions.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/RefLemma.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/RefSepRef.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/RefSeparated.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/RefSeparating.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/Rolle.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/StrongIVT.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/Taylor.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/TaylorLemma.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/ftc/WeakIVT.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/metrics/CMetricSpaces.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/metrics/CPMSTheory.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/metrics/CPseudoMSpaces.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/metrics/ContFunctions.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/metrics/Equiv.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/metrics/IR_CPMSpace.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/metrics/Prod_Sub.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/abgroups/QSposabgroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/abgroups/Qabgroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/abgroups/Qposabgroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/abgroups/Zabgroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/fields/Qfield.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/groups/QSposgroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/groups/Qgroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/groups/Qposgroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/groups/Zgroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/monoids/Nmonoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/monoids/Nposmonoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/monoids/QSposmonoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/monoids/Qmonoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/monoids/Qposmonoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/monoids/Zmonoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/non_examples/N_no_group.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/non_examples/Npos_no_group.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/non_examples/Npos_no_monoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/ordfields/Qordfield.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/reals/Cauchy_IR.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/rings/Qring.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/rings/Zring.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/semigroups/Npossemigroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/semigroups/Nsemigroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/semigroups/QSpossemigroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/semigroups/Qpossemigroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/semigroups/Qsemigroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/semigroups/Zsemigroup.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/setoids/Npossetoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/setoids/Nsetoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/setoids/Qpossetoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/setoids/Qsetoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/setoids/Zsetoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/structures/Npossec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/structures/Nsec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/structures/Qpossec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/structures/Qsec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/model/structures/Zsec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/preamble.ma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/Bridges_LUB.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/Bridges_iso.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/CMetricFields.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/CPoly_Contin.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/CReals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/CReals1.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/CSumsReals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/CauchySeq.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/Cauchy_CReals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/IVT.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/Intervals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/Max_AbsIR.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/NRootIR.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/OddPolyRootIR.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/Q_dense.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/Q_in_CReals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/R_morphism.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/RealFuncts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/RealLists.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/Series.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/reals/iso_CReals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/root [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/AlgReflection.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/DiffTactics1.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/DiffTactics2.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/DiffTactics3.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/FieldReflection.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/GroupReflection.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/Opaque_algebra.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/RingReflection.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/Step.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/tactics/Transparent_algebra.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/Exponential.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/InvTrigonom.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/Pi.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/PowerSeries.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/RealPowers.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/SinCos.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/TaylorSeries.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/TrigMon.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/CoRN/transc/Trigonometric.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Arith.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Between.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Bool_nat.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Compare.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Compare_dec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Div.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Div2.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/EqNat.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Euclid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Even.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Factorial.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Gt.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Le.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Lt.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Max.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Min.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Minus.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Mult.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Peano_dec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Plus.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Arith/Wf_nat.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Bool/Bool.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Bool/BoolEq.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Bool/DecBool.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Bool/IfProp.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Bool/Sumbool.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Bool/Zerob.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Coq.conf.xml [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Coq.ma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Init/Datatypes.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Init/Logic.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Init/Logic_Type.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Init/Notations.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Init/Peano.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Init/Prelude.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Init/Specif.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Init/Wf.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Adalloc.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Addec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Addr.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Adist.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Allmaps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Fset.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Lsort.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Map.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Mapaxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Mapc.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Mapcanon.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Mapcard.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Mapfold.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Mapiter.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Maplists.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/IntMap/Mapsubset.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Lists/List.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Lists/ListSet.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Lists/MonoList.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Lists/TheoryList.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Berardi.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/ChoiceFacts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Classical.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalChoice.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalFacts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Pred_Set.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Pred_Type.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Prop.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Type.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Decidable.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Diaconescu.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Eqdep_dec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/Hurkens.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/JMeq.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/ProofIrrelevance.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Logic/RelationalChoice.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Makefile [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/NArith/BinNat.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/NArith/BinPos.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/NArith/NArith.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/NArith/Pnat.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/AddProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Axioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/DiscrAxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/DiscrProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/EqAxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/GtAxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/LeAxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/NSyntax.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/NeqDef.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/OppAxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/OppProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/Params.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Num/SubProps.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Alembert.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/AltSeries.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/ArithProp.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Binomial.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Cauchy_prod.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Cos_plus.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Cos_rel.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/DiscrR.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Exp_prop.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Integration.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/MVT.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/NewtonInt.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/PSeries_reg.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/PartSum.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/RIneq.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/RList.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/R_Ifp.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/R_sqr.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/R_sqrt.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis1.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis2.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis3.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis4.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Raxioms.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rbase.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rbasic_fun.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rcomplete.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rdefinitions.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rderiv.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Reals.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rfunctions.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rgeom.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt_SF.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rlimit.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rpower.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rseries.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rsigma.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rsqrt_def.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rtopology.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_alt.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_calc.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_def.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_fun.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_reg.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/SeqProp.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/SeqSeries.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/SplitAbsolu.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/SplitRmult.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Reals/Sqrt_reg.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Relations/Newman.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Relations/Operators_Properties.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Relations/Relation_Definitions.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Relations/Relation_Operators.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Relations/Relations.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Relations/Rstar.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Setoids/Setoid.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Classical_sets.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Constructive_sets.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Cpo.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Ensembles.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Finite_sets.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Finite_sets_facts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Image.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Infinite_sets.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Integers.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Multiset.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Partial_Order.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Permut.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Powerset.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Powerset_Classical_facts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Powerset_facts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Relations_1.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Relations_1_facts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Relations_2.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Relations_2_facts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Relations_3.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Relations_3_facts.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sets/Uniset.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sorting/Heap.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sorting/Permutation.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Sorting/Sorting.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Disjoint_Union.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Inclusion.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Inverse_Image.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Lexicographic_Exponentiation.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Lexicographic_Product.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Transitive_Closure.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Union.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Well_Ordering.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/Wellfounded/Wellfounded.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/BinInt.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Wf_Z.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith_base.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith_dec.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zabs.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zbool.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zcompare.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zcomplements.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zdiv.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zeven.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zhints.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zlogarithm.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zmin.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zmisc.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Znat.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Znumtheory.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zorder.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zpower.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zsqrt.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/Zwf.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/ZArith/auxiliary.mma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/preamble.ma [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Coq/root [new file with mode: 0644] blob
helm/software/matita/contribs/procedural/Makefile.common [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.