--- a/src/HOL/PreList.thy Tue Aug 09 15:44:24 2005 +0200
+++ b/src/HOL/PreList.thy Tue Aug 09 19:10:30 2005 +0200
@@ -14,7 +14,4 @@
Is defined separately to serve as a basis for theory ToyList in the
documentation. *}
-lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
- -- {* belongs to theory @{text Wellfounded_Recursion} *}
-
end
--- a/src/HOL/Wellfounded_Recursion.thy Tue Aug 09 15:44:24 2005 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy Tue Aug 09 19:10:30 2005 +0200
@@ -56,6 +56,8 @@
|] ==> P(a)"
by (unfold wf_def, blast)
+lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
+
lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r"
by (erule_tac a=a in wf_induct, blast)