equal
deleted
inserted
replaced
111 (* types *) |
111 (* types *) |
112 |
112 |
113 val _ = |
113 val _ = |
114 OuterSyntax.command "typedecl" "type declaration" K.thy_decl |
114 OuterSyntax.command "typedecl" "type declaration" K.thy_decl |
115 (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => |
115 (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => |
116 Toplevel.theory (Typedecl.add (a, args, mx) #> snd))); |
116 Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd))); |
117 |
117 |
118 val _ = |
118 val _ = |
119 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
119 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
120 (Scan.repeat1 |
120 (Scan.repeat1 |
121 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) |
121 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) |