src/HOL/Real/Float.thy

--- a/src/HOL/Real/Float.thy	Thu Sep 28 23:42:43 2006 +0200
+++ b/src/HOL/Real/Float.thy	Thu Sep 28 23:42:45 2006 +0200
@@ -7,6 +7,7 @@
 
 theory Float
 imports Real
+uses ("float.ML")
 begin
 
 definition
@@ -521,4 +522,6 @@
 (* for use with the compute oracle *)
 lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
 
+use "float.ML";
+
 end