]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 885b29a) | patch
- new library/logic/coimplication.ma uses new decompose tactic
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Nov 2006 17:29:53 +0000 (17:29 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Nov 2006 17:29:53 +0000 (17:29 +0000)
commit62596f4e0a109e43c9df5da20571827c8b905ce4
tree90ed268409e97867e6f8c2aa6621ee457f8fd18btree | snapshot
parent885b29af55a246589b6a8966d9d1438fbb8155d3commit | diff
- new library/logic/coimplication.ma uses new decompose tactic
- matitaScript.ml: new parameter of inline tactic now ignored
- CoRN-Decl: regenerated with local objects handled correctly
109 files changed:
matita/contribs/CoRN-Decl/algebra/Basics.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CAbGroups.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CFields.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CGroups.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CLogic.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CMonoids.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/COrdAbs.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/COrdFields.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/COrdFields2.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CPolynomials.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CRings.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CSetoids.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CSums.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/Expon.ma diff | blob | history
matita/contribs/CoRN-Decl/algebra/ListType.ma diff | blob | history
matita/contribs/CoRN-Decl/complex/AbsCC.ma diff | blob | history
matita/contribs/CoRN-Decl/complex/CComplex.ma diff | blob | history
matita/contribs/CoRN-Decl/complex/NRootCC.ma diff | blob | history
matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/CC_Props.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/FTA.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/FTAreg.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/KeyLemma.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/KneserLemma.ma diff | blob | history
matita/contribs/CoRN-Decl/fta/MainLemma.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/Composition.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/Continuity.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/Derivative.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/Differentiability.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/FTC.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/FunctSequence.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/FunctSeries.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/Integral.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/NthDerivative.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/PartInterval.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/Partitions.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/RefLemma.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/RefSepRef.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/RefSeparated.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/RefSeparating.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/Rolle.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/StrongIVT.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/Taylor.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma diff | blob | history
matita/contribs/CoRN-Decl/ftc/WeakIVT.ma diff | blob | history
matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma diff | blob | history
matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma diff | blob | history
matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma diff | blob | history
matita/contribs/CoRN-Decl/metrics/ContFunctions.ma diff | blob | history
matita/contribs/CoRN-Decl/metrics/Equiv.ma diff | blob | history
matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma diff | blob | history
matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma diff | blob | history
matita/contribs/CoRN-Decl/model/structures/Qsec.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/Bridges_LUB.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/Bridges_iso.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/CMetricFields.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/CReals1.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/CSumsReals.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/CauchySeq.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/Cauchy_CReals.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/IVT.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/Intervals.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/NRootIR.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/OddPolyRootIR.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/Q_dense.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/R_morphism.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/RealFuncts.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/RealLists.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/Series.ma diff | blob | history
matita/contribs/CoRN-Decl/reals/iso_CReals.ma diff | blob | history
matita/contribs/CoRN-Decl/tactics/AlgReflection.ma diff | blob | history
matita/contribs/CoRN-Decl/tactics/DiffTactics2.ma diff | blob | history
matita/contribs/CoRN-Decl/tactics/FieldReflection.ma diff | blob | history
matita/contribs/CoRN-Decl/tactics/GroupReflection.ma diff | blob | history
matita/contribs/CoRN-Decl/tactics/RingReflection.ma diff | blob | history
matita/contribs/CoRN-Decl/transc/InvTrigonom.ma diff | blob | history
matita/contribs/CoRN-Decl/transc/Pi.ma diff | blob | history
matita/contribs/CoRN-Decl/transc/PowerSeries.ma diff | blob | history
matita/contribs/CoRN-Decl/transc/RealPowers.ma diff | blob | history
matita/contribs/CoRN-Decl/transc/SinCos.ma diff | blob | history
matita/contribs/CoRN-Decl/transc/TaylorSeries.ma diff | blob | history
matita/contribs/CoRN-Decl/transc/TrigMon.ma diff | blob | history
matita/contribs/CoRN-Decl/transc/Trigonometric.ma diff | blob | history
matita/library/logic/coimplication.ma [new file with mode: 0644] blob
matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.