- "big tree" order implemented

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / notation.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 71e9fae60b8616a3cc56917a0c12e8d55a397187..d2008a3f8a00f12c41f90026652677baf05c812f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -340,6 +340,10 @@ notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ break ⦃ term 46 L2 ⦄ )"
    non associative with precedence 45
    for @{ 'FocalizedPRedAlt $L1 $L2 }.
 
+notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'BTSuccessor $h $g $L1 $T1 $L2 $T2 }.
+
 (* Computation **************************************************************)
 
 notation "hvbox( T1 ➡ * break term 46 T2 )"
@@ -402,6 +406,10 @@ notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • * ⬊ * break [ ter
    non associative with precedence 45
    for @{ 'DecomposedXSN $h $g $L $T }.
 
+notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ > break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'BTGreaterThan $h $g $L1 $T1 $L2 $T2 }.
+
 (* Conversion ***************************************************************)
 
 notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"