equal
deleted
inserted
replaced
272 end |
272 end |
273 |
273 |
274 |
274 |
275 (* nominal *) |
275 (* nominal *) |
276 val _ = |
276 val _ = |
277 Outer_Syntax.local_theory_to_proof' ("nominal_primrec", Keyword.thy_goal) |
277 Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_primrec"} |
278 "define general recursive nominal functions" |
278 "define general recursive nominal functions" |
279 (nominal_function_parser nominal_default_config |
279 (nominal_function_parser nominal_default_config |
280 >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) |
280 >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) |
281 |
281 |
282 |
282 |