equal
deleted
inserted
replaced
190 |
190 |
191 fun fun_cmd fixes statements lthy = |
191 fun fun_cmd fixes statements lthy = |
192 lthy |
192 lthy |
193 |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config |
193 |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config |
194 ||> by_pat_completeness_simp |
194 ||> by_pat_completeness_simp |
195 (*|-> termination_by_lexicographic_order*) |> snd |
195 |-> termination_by_lexicographic_order |
196 |
196 |
197 |
197 |
198 val funP = |
198 val funP = |
199 OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl |
199 OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl |
200 ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow) |
200 ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow) |