]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/notation.ma
commit completed! some bugs fixed and some instances of auto resized
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / notation.ma
index 3ff8f21e555ec1a47cc980c76bf5585c50911562..7286479263a8d96775ee9d208d617631992aa3f5 100644 (file)
@@ -370,7 +370,7 @@ notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ ➡ * break ⦃ term 46 L2
    non associative with precedence 45
    for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }.
 
-notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ Tterm 46 2 ⦄ )"
+notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
    non associative with precedence 45
    for @{ 'PEval $L $T1 $T2 }.