diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -62,10 +62,9 @@
 using assms unfolding closed_def
 using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
 
-lemma not_open_ereal_singleton:
-  "\<not> (open {a :: ereal})"
-proof(rule ccontr)
-  assume "\<not> \<not> open {a}" hence a: "open {a}" by auto
+instance ereal :: perfect_space
+proof (default, rule)
+  fix a :: ereal assume a: "open {a}"
   show False
   proof (cases a)
     case MInf
@@ -138,7 +137,7 @@
   { assume "Inf S=(-\<infinity>)" hence False using * assms(3) by auto }
   moreover
   { assume "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`)
-    hence False by (metis assms(1) not_open_ereal_singleton) }
+    hence False by (metis assms(1) not_open_singleton) }
   moreover
   { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
     from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this