simp del: empty_Collect_eq;
authorwenzelm
Sat Dec 17 01:58:41 2005 +0100 (2005-12-17)
changeset 1842942ee9f24f63a
parent 18428 4059413acbc1
child 18430 46c18c0b52c1
simp del: empty_Collect_eq;
src/HOL/Real/PReal.thy
     1.1 --- a/src/HOL/Real/PReal.thy	Sat Dec 17 01:00:40 2005 +0100
     1.2 +++ b/src/HOL/Real/PReal.thy	Sat Dec 17 01:58:41 2005 +0100
     1.3 @@ -139,7 +139,7 @@
     1.4  subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
     1.5  
     1.6  lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
     1.7 -apply (auto simp add: preal_def cut_def intro: order_less_trans)
     1.8 +apply (auto simp del: empty_Collect_eq simp add: preal_def cut_def intro: order_less_trans)
     1.9  apply (force simp only: eq_commute [of "{}"] interval_empty_iff)
    1.10  apply (blast dest: dense intro: order_less_trans)
    1.11  done