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