# HG changeset patch
# User nipkow
# Date 1123607430 -7200
# Node ID da5cfaa258f780eee06de5809177509254ee8bcb
# Parent  dee6f7047cae0028b781add46a66b4a9592852cd
moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy

diff -r dee6f7047cae -r da5cfaa258f7 src/HOL/PreList.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
diff -r dee6f7047cae -r da5cfaa258f7 src/HOL/Wellfounded_Recursion.thy
--- 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)