X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdepends;h=f98e795f219b0966b8d395954edbf4c9e975dba6;hb=5978b976f9e1a2679e2b4ecc3c9984afdf2d5e11;hp=27032d916ef9ebfc92dcab808afd5a0a8deef3f1;hpb=6a16a37b5b4cbea5f5216247182d5bb99a0d8d65;p=helm.git

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index 27032d916..f98e795f2 100644
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -19,12 +19,13 @@ Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
 nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
 list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
 datatypes/compare.ma 
+didactic/exercises/substitution.ma nat/minus.ma
 nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma
 formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma
 logic/connectives.ma 
 Q/nat_fact/times.ma nat/factorization.ma
 decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
-demo/natural_deduction_support.ma 
+didactic/exercises/duality.ma nat/minus.ma
 nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
 nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
 nat/times.ma nat/plus.ma
@@ -50,10 +51,12 @@ nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
 demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
 list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma
 nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma
+didactic/support/natural_deduction.ma 
 nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma
 nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
 formal_topology/basic_pairs.ma datatypes/categories.ma formal_topology/relations.ma
 Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma nat/nat.ma
+didactic/exercises/shannon.ma nat/minus.ma
 Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma
 formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma
 nat/minus.ma nat/compare.ma nat/le_arith.ma
@@ -69,8 +72,8 @@ formal_topology/relations.ma datatypes/subsets.ma
 nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
 Z/moebius.ma Z/sigma_p.ma nat/factorization.ma
 demo/toolbox.ma logic/cprop_connectives.ma
-nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
 logic/coimplication.ma logic/connectives.ma
+nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
 nat/minimization.ma nat/minus.ma
 logic/connectives2.ma higher_order_defs/relations.ma
 datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma
@@ -80,10 +83,10 @@ Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma
 nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma
 nat/nat.ma higher_order_defs/functions.ma
 Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
-demo/natural_deduction.ma 
+demo/natural_deduction.ma didactic/support/natural_deduction.ma
 higher_order_defs/ordering.ma logic/equality.ma
-nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
 logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma
+nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
 nat/gcd.ma nat/lt_arith.ma nat/primes.ma
 datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
 Z/compare.ma Z/orders.ma nat/compare.ma
@@ -105,6 +108,7 @@ Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
 nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
 nat/gcd_properties1.ma nat/gcd.ma
 list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma
+didactic/exercises/natural_deduction.ma didactic/support/natural_deduction.ma
 Z/times.ma Z/plus.ma nat/lt_arith.ma
 Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
 nat/o.ma nat/binomial.ma nat/sqrt.ma