src/HOL/UNITY/ProgressSets.thy
changeset 32139 e271a64f03ff
parent 30198 922f944f03b2
child 32604 8b3e2bc91a46
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Wed Jul 22 14:21:52 2009 +0200
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Wed Jul 22 18:02:10 2009 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  lemma UN_in_lattice:
     1.6       "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
     1.7 -apply (simp add: Set.UN_eq) 
     1.8 +apply (simp add: UN_eq) 
     1.9  apply (blast intro: Union_in_lattice) 
    1.10  done
    1.11