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