equal
deleted
inserted
replaced
222 |
222 |
223 fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) = |
223 fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) = |
224 domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) |
224 domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) |
225 |
225 |
226 val _ = |
226 val _ = |
227 Outer_Syntax.command "domaindef" "HOLCF definition of domains from deflations" Keyword.thy_decl |
227 Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations" |
228 (domaindef_decl >> |
228 (domaindef_decl >> |
229 (Toplevel.print oo (Toplevel.theory o mk_domaindef))) |
229 (Toplevel.print oo (Toplevel.theory o mk_domaindef))) |
230 |
230 |
231 end |
231 end |