(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ⋓ break [ term 46 T , break term 46 l ] break term 46 L2 ≡ break term 46 L )"
+notation "hvbox( L1 ⋓ break [ term 46 T , break term 46 f ] break term 46 L2 ≡ break term 46 L )"
non associative with precedence 45
- for @{ 'LazyOr $L1 $T $l $L2 $L }.
+ for @{ 'LazyOr $L1 $T $f $L2 $L }.