# HG changeset patch
# User nipkow
# Date 1134980348 -3600
# Node ID 51a99fff78b2f7e3c00725afd67d50542700ffad
# Parent  0b596274ba4f271fe966244d78ed7003923efb16
fixed proof

diff -r 0b596274ba4f -r 51a99fff78b2 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Sun Dec 18 20:10:15 2005 +0100
+++ b/src/HOL/Real/PReal.thy	Mon Dec 19 09:19:08 2005 +0100
@@ -139,8 +139,8 @@
 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 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 (auto simp add: preal_def cut_def intro: order_less_trans)
+apply (blast dest:dense)
 apply (blast dest: dense intro: order_less_trans)
 done