--- a/src/HOL/Tools/recdef.ML Mon Nov 26 13:54:43 2012 +0100
+++ b/src/HOL/Tools/recdef.ML Mon Nov 26 14:43:28 2012 +0100
@@ -302,7 +302,7 @@
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
val _ =
- Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (TFL)"
+ Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
(recdef_decl >> Toplevel.theory);
@@ -314,12 +314,12 @@
val _ =
Outer_Syntax.command @{command_spec "defer_recdef"}
- "defer general recursive functions (TFL)"
+ "defer general recursive functions (obsolete TFL)"
(defer_recdef_decl >> Toplevel.theory);
val _ =
Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
- "recommence proof of termination condition (TFL)"
+ "recommence proof of termination condition (obsolete TFL)"
((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));