equal
deleted
inserted
replaced
260 then add_domain_cmd specs |
260 then add_domain_cmd specs |
261 else add_new_domain_cmd specs |
261 else add_new_domain_cmd specs |
262 end |
262 end |
263 |
263 |
264 val _ = |
264 val _ = |
265 Outer_Syntax.command "domain" "define recursive domains (HOLCF)" |
265 Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)" |
266 Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain)) |
266 (domains_decl >> (Toplevel.theory o mk_domain)) |
267 |
267 |
268 end |
268 end |