(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation > "hvbox( T . break ②{ term 46 I } break term 47 T1 )"
- non associative with precedence 46
- for @{ 'DxBind2 $T $I $T1 }.
-
-notation "hvbox( T . break ⓑ { term 46 I } break term 48 T1 )"
- non associative with precedence 47
- for @{ 'DxBind2 $T $I $T1 }.
+notation "hvbox( L. break ⓑ { term 46 I } break term 49 T1 )"
+ non associative with precedence 48
+ for @{ 'DxBind2 $L $I $T1 }.