src/HOL/Wellfounded.thy
changeset 44937 22c0857b8aab
parent 44921 58eef4843641
child 45012 060f76635bfe
     1.1 --- a/src/HOL/Wellfounded.thy	Thu Sep 15 17:06:00 2011 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Thu Sep 15 12:40:08 2011 -0400
     1.3 @@ -305,9 +305,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 -apply (simp add: Union_def)
     1.8 -apply (blast intro: wf_UN)
     1.9 -done
    1.10 +  using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
    1.11  
    1.12  (*Intuition: we find an (R u S)-min element of a nonempty subset A
    1.13               by case distinction.