branch for universe

[helm.git] / matita / contribs / CoRN-Decl / ordine_compilazione.txt

diff --git a/matita/contribs/CoRN-Decl/ordine_compilazione.txt b/matita/contribs/CoRN-Decl/ordine_compilazione.txt
new file mode 100644 (file)
index 0000000..2770903
--- /dev/null
+++ b/matita/contribs/CoRN-Decl/ordine_compilazione.txt
@@ -0,0 +1,157 @@
+CoRN.ma                                OK
+algebra/ListType.ma
+algebra/Basics.ma
+algebra/CLogic.ma
+tactics/Step.ma
+algebra/CSetoids.ma
+algebra/CSetoidFun.ma
+algebra/CSetoidInc.ma
+algebra/CSemiGroups.ma
+algebra/CMonoids.ma
+algebra/CGroups.ma
+algebra/CAbGroups.ma
+algebra/CAbMonoids.ma
+algebra/CSums.ma
+algebra/CRings.ma
+algebra/CFields.ma
+tactics/AlgReflection.ma
+tactics/Opaque_algebra.ma
+tactics/FieldReflection.ma
+tactics/Transparent_algebra.ma
+algebra/COrdFields.ma
+algebra/COrdFields2.ma
+algebra/COrdAbs.ma
+algebra/COrdCauchy.ma
+tactics/RingReflection.ma
+algebra/CPolynomials.ma
+algebra/CPoly_NthCoeff.ma
+algebra/CPoly_Degree.ma
+algebra/CPoly_ApZero.ma
+algebra/CVectorSpace.ma
+algebra/Cauchy_COF.ma
+algebra/Expon.ma
+reals/CReals.ma
+reals/CauchySeq.ma
+reals/Max_AbsIR.ma
+reals/CReals1.ma
+reals/RealFuncts.ma
+reals/CPoly_Contin.ma
+reals/IVT.ma
+reals/OddPolyRootIR.ma
+reals/NRootIR.ma
+complex/CComplex.ma
+complex/AbsCC.ma
+reals/RealLists.ma
+reals/Intervals.ma
+tactics/DiffTactics1.ma
+ftc/PartFunEquality.ma
+reals/CSumsReals.ma
+ftc/FunctSums.ma
+ftc/Continuity.ma
+ftc/Derivative.ma
+ftc/DerivativeOps.ma
+ftc/IntervalFunct.ma
+ftc/PartInterval.ma
+ftc/Differentiability.ma
+ftc/NthDerivative.ma
+ftc/MoreIntervals.ma
+ftc/MoreFunctions.ma
+tactics/DiffTactics2.ma
+ftc/Rolle.ma
+ftc/TaylorLemma.ma
+ftc/Taylor.ma
+ftc/Composition.ma
+ftc/FunctSequence.ma
+reals/Series.ma
+ftc/FunctSeries.ma
+ftc/MoreFunSeries.ma
+tactics/DiffTactics3.ma
+ftc/CalculusTheorems.ma
+ftc/COrdLemmas.ma
+ftc/Partitions.ma
+ftc/RefSepRef.ma
+ftc/RefSeparated.ma
+ftc/RefSeparating.ma
+ftc/RefLemma.ma
+ftc/Integral.ma
+ftc/MoreIntegrals.ma
+ftc/FTC.ma
+transc/PowerSeries.ma
+transc/TaylorSeries.ma
+transc/Exponential.ma
+transc/Trigonometric.ma
+transc/SinCos.ma
+transc/Pi.ma
+complex/Complex_Exponential.ma
+complex/NRootCC.ma
+devel/loeb/per/csetfun.ma
+devel/loeb/per/lst2fun.ma
+model/structures/Nsec.ma
+model/setoids/Nsetoid.ma
+model/semigroups/Nsemigroup.ma
+model/monoids/Nmonoid.ma
+model/structures/Zsec.ma
+model/setoids/Zsetoid.ma
+model/semigroups/Zsemigroup.ma
+model/monoids/Zmonoid.ma
+model/structures/Qsec.ma
+model/setoids/Qsetoid.ma
+devel/loeb/IDA/Ch6.ma
+fta/CC_Props.ma
+fta/CPoly_Contin1.ma
+fta/CPoly_Rev.ma
+fta/CPoly_Shift.ma
+fta/KeyLemma.ma
+fta/MainLemma.ma
+fta/KneserLemma.ma
+fta/FTAreg.ma
+fta/FTA.ma
+ftc/WeakIVT.ma
+ftc/StrongIVT.ma
+metrics/CPseudoMSpaces.ma
+metrics/ContFunctions.ma
+metrics/IR_CPMSpace.ma
+metrics/Equiv.ma
+metrics/Prod_Sub.ma
+metrics/CMetricSpaces.ma
+metrics/CPMSTheory.ma
+model/structures/Qpossec.ma
+model/setoids/Qpossetoid.ma
+model/semigroups/QSpossemigroup.ma
+model/monoids/QSposmonoid.ma
+model/groups/QSposgroup.ma
+model/abgroups/QSposabgroup.ma
+model/semigroups/Qsemigroup.ma
+model/monoids/Qmonoid.ma
+model/groups/Qgroup.ma
+model/abgroups/Qabgroup.ma
+model/semigroups/Qpossemigroup.ma
+model/monoids/Qposmonoid.ma
+model/groups/Qposgroup.ma
+model/abgroups/Qposabgroup.ma
+model/groups/Zgroup.ma
+model/abgroups/Zabgroup.ma
+model/rings/Zring.ma
+model/rings/Qring.ma
+model/fields/Qfield.ma
+model/structures/Npossec.ma
+model/setoids/Npossetoid.ma
+model/semigroups/Npossemigroup.ma
+model/monoids/Nposmonoid.ma
+model/non_examples/N_no_group.ma
+model/non_examples/Npos_no_group.ma
+model/non_examples/Npos_no_monoid.ma
+model/ordfields/Qordfield.ma
+reals/Cauchy_CReals.ma
+model/reals/Cauchy_IR.ma
+reals/Q_in_CReals.ma
+reals/Q_dense.ma
+reals/R_morphism.ma
+reals/iso_CReals.ma
+reals/Bridges_LUB.ma
+reals/Bridges_iso.ma
+reals/CMetricFields.ma
+tactics/GroupReflection.ma
+transc/RealPowers.ma
+transc/TrigMon.ma
+transc/InvTrigonom.ma