]> matita.cs.unibo.it Git - helm.git/commitdiff
changed default divide notation to a/b
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 26 Sep 2005 09:29:59 +0000 (09:29 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 26 Sep 2005 09:29:59 +0000 (09:29 +0000)
helm/matita/core_notation.moo

index a2802c3da8eabd6d5bb5176c7323f1e388724c31..449108cd9f9175d8703e8e99cdf1aa358e6d6f96 100644 (file)
@@ -66,9 +66,9 @@ notation "hvbox(a break * b)"
   left associative with precedence 55
 for @{ 'times $a $b }.
 
-notation "hvbox(a break / b)" 
+notation "hvbox(a break % b)" 
   left associative with precedence 55
-for @{ 'divide $a $b }.
+for @{ 'module $a $b }.
 
 notation "\frac a b" 
   non associative with precedence 90
@@ -78,6 +78,10 @@ notation "a \over b"
   left associative with precedence 55
 for @{ 'divide $a $b }.
 
+notation "hvbox(a break / b)" 
+  left associative with precedence 55
+for @{ 'divide $a $b }.
+
 notation > "- a" 
   right associative with precedence 60
 for @{ 'uminus $a }.