equal
deleted
inserted
replaced
168 fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b c tac int) |
168 fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b c tac int) |
169 |
169 |
170 |
170 |
171 |
171 |
172 val _ = |
172 val _ = |
173 Outer_Syntax.local_theory' "fun" "define general recursive functions (short version)" |
173 Outer_Syntax.local_theory' @{command_spec "fun"} |
174 Keyword.thy_decl |
174 "define general recursive functions (short version)" |
175 (function_parser fun_config |
175 (function_parser fun_config |
176 >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config)) |
176 >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config)) |
177 |
177 |
178 end |
178 end |