--- a/src/HOL/Real/Float.thy Tue Jul 19 17:28:27 2005 +0200
+++ b/src/HOL/Real/Float.thy Tue Jul 19 17:28:37 2005 +0200
@@ -3,7 +3,7 @@
Author: Steven Obua
*)
-theory Float = Real:
+theory Float imports Real begin
constdefs
pow2 :: "int \<Rightarrow> real"