From: Enrico Tassi Date: Thu, 25 May 2006 14:10:17 +0000 (+0000) Subject: added a file useful to load all notation X-Git-Tag: 0.4.95@7852~1433 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=adeaf656f62574342585ccaf29554c3f3ed526f8;p=helm.git added a file useful to load all notation (use include' and not include). --- diff --git a/matita/library/library_notation.ma b/matita/library/library_notation.ma new file mode 100644 index 000000000..45f841d64 --- /dev/null +++ b/matita/library/library_notation.ma @@ -0,0 +1,54 @@ +set "baseuri" "cic:/matita/library_notation/". + +include "Q/q.ma". +include "higher_order_defs/functions.ma". +include "higher_order_defs/ordering.ma". +include "higher_order_defs/relations.ma". +include "nat/nth_prime.ma". +include "nat/plus.ma". +include "nat/ord.ma". +include "nat/congruence.ma". +include "nat/compare.ma". +include "nat/totient.ma". +include "nat/le_arith.ma". +include "nat/count.ma". +include "nat/orders.ma". +include "nat/minus.ma". +include "nat/exp.ma". +include "nat/gcd.ma". +include "nat/div_and_mod.ma". +include "nat/primes.ma". +include "nat/relevant_equations.ma". +include "nat/chinese_reminder.ma". +include "nat/factorial.ma". +include "nat/lt_arith.ma". +include "nat/minimization.ma". +include "nat/permutation.ma". +include "nat/sigma_and_pi.ma". +include "nat/factorization.ma". +include "nat/primes1.ma". +include "nat/times.ma". +include "nat/fermat_little_theorem.ma". +include "nat/nat.ma". +include "legacy/coq.ma". +include "Z/compare.ma". +include "Z/plus.ma". +include "Z/times.ma". +include "Z/z.ma". +include "Z/orders.ma". +include "list/sort.ma". +include "list/list.ma". +include "algebra/semigroups.ma". +include "algebra/monoids.ma". +include "algebra/groups.ma". +include "algebra/finite_groups.ma". +include "logic/connectives.ma". +include "logic/equality.ma". +include "datatypes/constructors.ma". +include "datatypes/compare.ma". +include "datatypes/bool.ma". + +notation "hvbox(x break \middot y)" + left associative with precedence 55 +for @{ 'times $x $y }. +