- transcript: we have now two styles of mma's from grafite:

[helm.git] / helm / software / matita / library / depends

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index 1afd0516ccc211c533e1d8ab835c8abff1b62ec7..4e5374dc7eb1a1d9e31f8c2485c7ad7ccff490f7 100644 (file)
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -1,4 +1,3 @@
-theory.ma Q/Qaxioms.ma Q/frac.ma Q/inv.ma Q/q/qplus.ma Q/q/qtimes.ma R/Rlog.ma Z/inversion.ma algebra/finite_groups.ma dama/models/nat_lebesgue.ma datatypes/subsets.ma decidable_kit/fgraph.ma demo/cantor.ma demo/natural_deduction.ma demo/power_derivative.ma demo/propositional_sequent_calculus.ma demo/realisability.ma demo/toolbox.ma didactic/exercises/duality.ma didactic/exercises/natural_deduction.ma didactic/exercises/natural_deduction1.ma didactic/exercises/natural_deduction_fst_order.ma didactic/exercises/natural_deduction_theories.ma didactic/exercises/shannon.ma didactic/exercises/substitution.ma nat/bertrand.ma nat/chebyshev_thm.ma nat/euler_theorem.ma nat/factorization2.ma nat/fermat_little_theorem.ma nat/totient1.ma technicalities/setoids.ma
 dama/sandwich.ma dama/ordered_uniform.ma
 demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma
 Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
@@ -19,7 +18,6 @@ algebra/groups.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_ari
 nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
 Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
 nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
-theory.ma Q/Qaxioms.ma Q/frac.ma Q/inv.ma Q/q/qplus.ma Q/q/qtimes.ma R/Rlog.ma Z/inversion.ma algebra/finite_groups.ma dama/models/nat_lebesgue.ma datatypes/subsets.ma decidable_kit/fgraph.ma demo/cantor.ma demo/natural_deduction.ma demo/power_derivative.ma demo/propositional_sequent_calculus.ma demo/realisability.ma demo/toolbox.ma didactic/exercises/duality.ma didactic/exercises/natural_deduction.ma didactic/exercises/natural_deduction1.ma didactic/exercises/natural_deduction_fst_order.ma didactic/exercises/natural_deduction_theories.ma didactic/exercises/shannon.ma didactic/exercises/substitution.ma nat/bertrand.ma nat/chebyshev_thm.ma nat/euler_theorem.ma nat/factorization2.ma nat/fermat_little_theorem.ma nat/totient1.ma technicalities/setoids.ma
 dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma
 list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
 datatypes/compare.ma