src/HOL/UNITY/ProgressSets.thy
changeset 44918 6a80fbc4e72c
parent 44106 0e018cbcc0de
child 45477 11d9c2768729
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Tue Sep 13 13:17:52 2011 +0200
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Tue Sep 13 16:21:48 2011 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4  by (simp add: cl_def, blast)
     1.5  
     1.6  lemma subset_cl: "r \<subseteq> cl L r"
     1.7 -by (simp add: cl_def, blast)
     1.8 +by (simp add: cl_def le_Inf_iff)
     1.9  
    1.10  text{*A reformulation of @{thm subset_cl}*}
    1.11  lemma clI: "x \<in> r ==> x \<in> cl L r"