changeset 1813 | 23bda45846a2 |
parent 1580 | e3fd931e6095 |
child 2202 | cc15a7bfbe12 |
--- a/src/Pure/Syntax/syntax.ML Tue Jun 18 16:20:30 1996 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Jun 18 16:27:04 1996 +0200 @@ -13,10 +13,6 @@ include SYN_TRANS0 include MIXFIX0 include PRINTER0 - datatype 'a trrule = - op |-> of 'a * 'a | - op <-| of 'a * 'a | - op <-> of 'a * 'a end; signature SYNTAX =