src/HOL/RComplete.thy
changeset 45966 03ce2b2a29a2
parent 44708 37ce74ff4203
child 46671 3a40ea076230
     1.1 --- a/src/HOL/RComplete.thy	Sat Dec 24 15:53:09 2011 +0100
     1.2 +++ b/src/HOL/RComplete.thy	Sat Dec 24 15:53:09 2011 +0100
     1.3 @@ -76,8 +76,7 @@
     1.4    from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y"
     1.5      unfolding isUb_def setle_def by simp_all
     1.6    from complete_real [OF this] show ?thesis
     1.7 -    unfolding isLub_def leastP_def setle_def setge_def Ball_def
     1.8 -      Collect_def mem_def isUb_def UNIV_def by simp
     1.9 +    by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
    1.10  qed
    1.11  
    1.12