]> matita.cs.unibo.it Git - helm.git/commitdiff
added a file useful to load all notation
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 25 May 2006 14:10:17 +0000 (14:10 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 25 May 2006 14:10:17 +0000 (14:10 +0000)
(use include' and not include).

matita/library/library_notation.ma [new file with mode: 0644]

diff --git a/matita/library/library_notation.ma b/matita/library/library_notation.ma
new file mode 100644 (file)
index 0000000..45f841d
--- /dev/null
@@ -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 }.
+