]> matita.cs.unibo.it Git - helm.git/commitdiff
removed unused notation =>
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 13 Oct 2007 13:17:59 +0000 (13:17 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 13 Oct 2007 13:17:59 +0000 (13:17 +0000)
matita/core_notation.moo

index 2ecb35e8be5b738afff7201ccf441199170652e5..17d5993b10a2a2d7ab0f14b88fa768a18da537d7 100644 (file)
@@ -119,7 +119,3 @@ for @{ 'and $a $b }.
 notation "hvbox(\lnot a)" 
   non associative with precedence 40
 for @{ 'not $a }.
-
-notation "hvbox(a break => b)" 
-  non associative with precedence 45
-for @{ 'parred $a $b }.