diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/SetInterval.thy	Fri Aug 28 18:52:41 2009 +0200
@@ -181,9 +181,10 @@
   "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
-text {* The above four lemmas could be declared as iffs.
-  If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
-  seems to take forever (more than one hour). *}
+text {* The above four lemmas could be declared as iffs. Unfortunately this
+breaks many proofs. Since it only helps blast, it is better to leave well
+alone *}
+
 end
 
 subsubsection{* Emptyness, singletons, subset *}