matita.cs.unibo.it Git - helm.git/commit - helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo

]> matita.cs.unibo.it Git - helm.git/commit - helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_fun.mma

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 5 Sep 2008 18:37:01 +0000 (18:37 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 5 Sep 2008 18:37:01 +0000 (18:37 +0000)
commit	f620bf94af6c347926ed1c2328462efab7018b21
tree	9fde04b63b99abecb50eb0e396ef7243a869f2ba	tree \| snapshot
parent	418b1f26ab67b824c79d1146fdb50ca29b34c1f6	commit \| diff

transcript: we now check for non-existing objects
procedural/Coq: we now generate from ufficial 8.0pl2
that does not have the Num directory

235 files changed:

helm/software/components/binaries/transcript/.depend.opt		diff \| blob \| history
helm/software/components/binaries/transcript/engine.ml		diff \| blob \| history
helm/software/components/binaries/transcript/engine.mli		diff \| blob \| history
helm/software/components/binaries/transcript/grafite.ml		diff \| blob \| history
helm/software/components/binaries/transcript/options.ml		diff \| blob \| history
helm/software/components/binaries/transcript/top.ml		diff \| blob \| history
helm/software/components/binaries/transcript/v8Parser.mly		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Arith.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Between.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Bool_nat.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Compare.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Compare_dec.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Div.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Div2.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/EqNat.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Euclid.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Even.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Factorial.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Gt.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Le.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Lt.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Max.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Min.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Minus.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Mult.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Peano_dec.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Plus.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Arith/Wf_nat.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/Bool.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/BoolEq.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/DecBool.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/IfProp.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/Sumbool.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Bool/Zerob.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Coq.conf.xml		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Coq.ma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Init/Datatypes.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Init/Logic.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Init/Logic_Type.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Init/Notations.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Init/Peano.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Init/Prelude.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Init/Specif.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Init/Wf.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Adalloc.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Addec.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Addr.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Adist.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Allmaps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Fset.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Lsort.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Map.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Mapaxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Mapc.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Mapcanon.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Mapcard.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Mapfold.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Mapiter.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Maplists.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/IntMap/Mapsubset.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Lists/List.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Lists/ListSet.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Lists/MonoList.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Lists/Streams.mma	[new file with mode: 0644]	blob
helm/software/matita/contribs/procedural/Coq/Lists/TheoryList.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Berardi.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/ChoiceFacts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Classical.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalChoice.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalFacts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Pred_Set.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Pred_Type.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Prop.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Type.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Decidable.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Diaconescu.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Eqdep_dec.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/Hurkens.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/JMeq.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/ProofIrrelevance.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Logic/RelationalChoice.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/NArith/BinNat.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/NArith/BinPos.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/NArith/NArith.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/NArith/Pnat.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/AddProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Axioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/DiscrAxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/DiscrProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/EqAxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/GtAxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/LeAxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/NSyntax.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/NeqDef.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/OppAxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/OppProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/Params.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Num/SubProps.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Alembert.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/AltSeries.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/ArithProp.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Binomial.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Cauchy_prod.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Cos_plus.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Cos_rel.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/DiscrR.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Exp_prop.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Integration.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/MVT.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/NewtonInt.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/PSeries_reg.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/PartSum.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/RIneq.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/RList.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/R_Ifp.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/R_sqr.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/R_sqrt.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis1.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis2.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis3.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis4.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Raxioms.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rbase.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rbasic_fun.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rcomplete.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rdefinitions.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rderiv.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Reals.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rfunctions.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rgeom.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt_SF.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rlimit.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rpower.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rseries.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rsigma.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rsqrt_def.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rtopology.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_alt.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_calc.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_def.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_fun.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_reg.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/SeqProp.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/SeqSeries.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/SplitAbsolu.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/SplitRmult.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Reals/Sqrt_reg.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Relations/Newman.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Relations/Operators_Properties.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Relations/Relation_Definitions.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Relations/Relation_Operators.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Relations/Relations.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Relations/Rstar.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Setoids/Setoid.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Classical_sets.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Constructive_sets.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Cpo.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Ensembles.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Finite_sets.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Finite_sets_facts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Image.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Infinite_sets.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Integers.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Multiset.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Partial_Order.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Permut.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Powerset.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Powerset_Classical_facts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Powerset_facts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Relations_1.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Relations_1_facts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Relations_2.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Relations_2_facts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Relations_3.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Relations_3_facts.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sets/Uniset.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sorting/Heap.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sorting/Permutation.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Sorting/Sorting.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Disjoint_Union.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Inclusion.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Inverse_Image.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Lexicographic_Exponentiation.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Lexicographic_Product.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Transitive_Closure.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Union.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Well_Ordering.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/Wellfounded/Wellfounded.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/BinInt.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Wf_Z.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith_base.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith_dec.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zabs.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zbool.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zcompare.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zcomplements.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zdiv.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zeven.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zhints.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zlogarithm.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zmin.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zmisc.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Znat.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Znumtheory.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zorder.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zpower.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zsqrt.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/Zwf.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Coq/ZArith/auxiliary.mma		diff \| blob \| history
helm/software/matita/contribs/procedural/Makefile.common		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom