From 00bba19fcd102e03db20f273740047b77a84be80 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 26 Sep 2005 09:29:59 +0000 Subject: [PATCH] changed default divide notation to a/b --- helm/matita/core_notation.moo | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo index a2802c3da..449108cd9 100644 --- a/helm/matita/core_notation.moo +++ b/helm/matita/core_notation.moo @@ -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 }. -- 2.39.2