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