src/HOL/Library/Float.thy

--- a/src/HOL/Library/Float.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Float.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
 
 definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
 
-typedef (open) float = float
+typedef float = float
   morphisms real_of_float float_of
   unfolding float_def by auto