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' "nominal_primrec" "define general recursive nominal functions" |
278 Outer_Syntax.local_theory_to_proof' ("nominal_primrec", Keyword.thy_goal) |
279 Keyword.thy_goal |
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 |
284 end |
284 end |