src/HOL/Wellfounded.thy
changeset 56166 9a241bc276cd
parent 55932 68c5104d2204
child 56218 1c3f1f2431f9
     1.1 --- a/src/HOL/Wellfounded.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -306,7 +306,7 @@
     1.4   "[| ALL r:R. wf r;  
     1.5       ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
     1.6    |] ==> wf(Union R)"
     1.7 -  using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
     1.8 +  using wf_UN[of R "\<lambda>i. i"] by simp
     1.9  
    1.10  (*Intuition: we find an (R u S)-min element of a nonempty subset A
    1.11               by case distinction.