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