# HG changeset patch
# User wenzelm
# Date 1134781121 -3600
# Node ID 42ee9f24f63af7ec45bc17d9c33d2b2df63e2c4d
# Parent  4059413acbc102c632b2825141df7eec7242eef4
simp del: empty_Collect_eq;

diff -r 4059413acbc1 -r 42ee9f24f63a src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Sat Dec 17 01:00:40 2005 +0100
+++ b/src/HOL/Real/PReal.thy	Sat Dec 17 01:58:41 2005 +0100
@@ -139,7 +139,7 @@
 subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
 
 lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
-apply (auto simp add: preal_def cut_def intro: order_less_trans)
+apply (auto simp del: empty_Collect_eq simp add: preal_def cut_def intro: order_less_trans)
 apply (force simp only: eq_commute [of "{}"] interval_empty_iff)
 apply (blast dest: dense intro: order_less_trans)
 done