# HG changeset patch
# User wenzelm
# Date 1159479765 -7200
# Node ID 89bec28a03c861b89512935df45d8b5c20091a28
# Parent  2c583720436e7b017d589373c43d94ba86ee8a69
proper use of float.ML;

diff -r 2c583720436e -r 89bec28a03c8 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