--- 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 *}