| changeset 9037 | 91cbae314c84 |
| parent 9032 | ad0b9f048bbf |
| child 9056 | 8f78b2aea39e |
| 9036:d9e09ef531dd | 9037:91cbae314c84 |
|---|---|
103 Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt)))); |
103 Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt)))); |
104 |
104 |
105 val typeabbrP = |
105 val typeabbrP = |
106 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
106 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
107 (Scan.repeat1 |
107 (Scan.repeat1 |
108 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix)) -- P.marg_comment) |
108 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')) -- P.marg_comment) |
109 >> (Toplevel.theory o IsarThy.add_tyabbrs o |
109 >> (Toplevel.theory o IsarThy.add_tyabbrs o |
110 map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt)))); |
110 map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt)))); |
111 |
111 |
112 val nontermP = |
112 val nontermP = |
113 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" |
113 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" |