equal
deleted
inserted
replaced
318 (defer_recdef_decl >> Toplevel.theory); |
318 (defer_recdef_decl >> Toplevel.theory); |
319 |
319 |
320 val _ = |
320 val _ = |
321 OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)" |
321 OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)" |
322 K.thy_goal |
322 K.thy_goal |
323 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname -- |
323 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname -- |
324 Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") |
324 Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") |
325 >> (fn ((thm_name, name), i) => recdef_tc thm_name name i)); |
325 >> (fn ((thm_name, name), i) => recdef_tc thm_name name i)); |
326 |
326 |
327 end; |
327 end; |
328 |
328 |