moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy

--- 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)