equal
deleted
inserted
replaced
300 lthy |
300 lthy |
301 |> FundefPackage.add_fundef fixes statements config flags |
301 |> FundefPackage.add_fundef fixes statements config flags |
302 |> by_pat_completeness_simp |
302 |> by_pat_completeness_simp |
303 |> termination_by_lexicographic_order |
303 |> termination_by_lexicographic_order |
304 |
304 |
305 val funP = |
305 val _ = |
306 OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl |
306 OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl |
307 (fundef_parser fun_config |
307 (fundef_parser fun_config |
308 >> (fn ((config, fixes), (flags, statements)) => |
308 >> (fn ((config, fixes), (flags, statements)) => |
309 (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags)))); |
309 (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags)))); |
310 |
310 |
311 val _ = OuterSyntax.add_parsers [funP]; |
|
312 end |
311 end |
313 |
312 |
314 end |
313 end |