changeset 2287 | 94b70aeb7d1f |
parent 2202 | cc15a7bfbe12 |
child 2366 | a163d2be1bb5 |
--- a/src/Pure/Syntax/syntax.ML Mon Dec 02 10:22:41 1996 +0100 +++ b/src/Pure/Syntax/syntax.ML Mon Dec 02 10:23:28 1996 +0100 @@ -25,9 +25,9 @@ include MIXFIX1 include PRINTER0 datatype 'a trrule = - op |-> of 'a * 'a | - op <-| of 'a * 'a | - op <-> of 'a * 'a + |-> of 'a * 'a | + <-| of 'a * 'a | + <-> of 'a * 'a type syntax val extend_log_types: syntax -> string list -> syntax val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax