# HG changeset patch
# User paulson
# Date 1149349782 -7200
# Node ID 031e0dde31f14253f28f1ef11f897768f3453582
# Parent  dfe9409116178648504b9225aa3355fa0ba38ba4
generalized wfI

diff -r dfe940911617 -r 031e0dde31f1 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Fri Jun 02 23:22:29 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Sat Jun 03 17:49:42 2006 +0200
@@ -42,11 +42,11 @@
    "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
 by (unfold wf_def, blast)
 
-text{*Restriction to domain @{term A}.  
-  If @{term r} is well-founded over @{term A} then @{term "wf r"}*}
+text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
+    well-founded over their intersection, then @{term "wf r"}*}
 lemma wfI: 
- "[| r <= A <*> A;   
-     !!x P. [| ALL x. (ALL y. (y,x) : r --> P y) --> P x;  x:A |] ==> P x |]   
+ "[| r \<subseteq> A <*> B; 
+     !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
   ==>  wf r"
 by (unfold wf_def, blast)