equal
deleted
inserted
replaced
2309 |
2309 |
2310 |
2310 |
2311 (* outer syntax *) |
2311 (* outer syntax *) |
2312 |
2312 |
2313 val _ = |
2313 val _ = |
2314 Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl |
2314 Outer_Syntax.command @{command_spec "record"} "define extensible record" |
2315 (Parse.type_args_constrained -- Parse.binding -- |
2315 (Parse.type_args_constrained -- Parse.binding -- |
2316 (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) -- |
2316 (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) -- |
2317 Scan.repeat1 Parse.const_binding) |
2317 Scan.repeat1 Parse.const_binding) |
2318 >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z))); |
2318 >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z))); |
2319 |
2319 |