src/HOL/Real/Float.thy
changeset 16890 c4e5afaba440
parent 16782 b214f21ae396
child 19765 dfe940911617
     1.1 --- a/src/HOL/Real/Float.thy	Tue Jul 19 17:28:27 2005 +0200
     1.2 +++ b/src/HOL/Real/Float.thy	Tue Jul 19 17:28:37 2005 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author: Steven Obua
     1.5  *)
     1.6  
     1.7 -theory Float = Real:
     1.8 +theory Float imports Real begin
     1.9  
    1.10  constdefs  
    1.11    pow2 :: "int \<Rightarrow> real"