equal
deleted
inserted
replaced
210 fun mk_domaindef (((((args, t)), mx), A), morphs) = |
210 fun mk_domaindef (((((args, t)), mx), A), morphs) = |
211 domaindef_cmd ((t, args, mx), A, morphs) |
211 domaindef_cmd ((t, args, mx), A, morphs) |
212 |
212 |
213 val _ = |
213 val _ = |
214 Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations" |
214 Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations" |
215 (domaindef_decl >> |
215 (domaindef_decl >> (Toplevel.theory o mk_domaindef)) |
216 (Toplevel.print oo (Toplevel.theory o mk_domaindef))) |
|
217 |
216 |
218 end |
217 end |