-(* this might be removed *)
-notation "hvbox( ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'HdReducible $T }.
-
-(* this might be removed *)
-notation "hvbox( L โข break ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'HdReducible $L $T }.
-
-(* this might be removed *)
-notation "hvbox( ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'NotHdReducible $T }.
-
-(* this might be removed *)
-notation "hvbox( L โข break ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'NotHdReducible $L $T }.
-
-(* this might be removed *)
-notation "hvbox( ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'HdNormal $T }.
-
-(* this might be removed *)
-notation "hvbox( L โข break ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'HdNormal $L $T }.
-