]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/library_notation.ma
More exceptions pretty-printed.
[helm.git] / helm / software / matita / library / library_notation.ma
1 set "baseuri" "cic:/matita/library_notation/".
2
3 include "Q/q.ma".
4 include "higher_order_defs/functions.ma".
5 include "higher_order_defs/ordering.ma".
6 include "higher_order_defs/relations.ma".
7 include "nat/nth_prime.ma".
8 include "nat/plus.ma".
9 include "nat/ord.ma".
10 include "nat/congruence.ma".
11 include "nat/compare.ma".
12 include "nat/totient.ma".
13 include "nat/le_arith.ma".
14 include "nat/count.ma".
15 include "nat/orders.ma".
16 include "nat/minus.ma".
17 include "nat/exp.ma".
18 include "nat/gcd.ma".
19 include "nat/div_and_mod.ma".
20 include "nat/primes.ma".
21 include "nat/relevant_equations.ma".
22 include "nat/chinese_reminder.ma".
23 include "nat/factorial.ma".
24 include "nat/lt_arith.ma".
25 include "nat/minimization.ma".
26 include "nat/permutation.ma".
27 include "nat/sigma_and_pi.ma".
28 include "nat/factorization.ma".
29 include "nat/times.ma".
30 include "nat/fermat_little_theorem.ma".
31 include "nat/nat.ma".
32 (* FG: coq non c'entra con library, o sbaglio? *)
33 (* include "legacy/coq.ma". *)
34 include "Z/compare.ma".
35 include "Z/plus.ma".
36 include "Z/times.ma".
37 include "Z/z.ma".
38 include "Z/orders.ma".
39 include "list/sort.ma".
40 include "list/list.ma".
41 include "algebra/semigroups.ma".
42 include "algebra/monoids.ma".
43 include "algebra/groups.ma".
44 include "algebra/finite_groups.ma". 
45 include "logic/connectives.ma".
46 include "logic/equality.ma".
47 include "datatypes/constructors.ma".
48 include "datatypes/compare.ma".
49 include "datatypes/bool.ma".
50
51 notation "hvbox(x break \middot y)"
52   left associative with precedence 55
53 for @{ 'times $x $y }.
54