proper use of float.ML;
authorwenzelm
Thu Sep 28 23:42:45 2006 +0200 (2006-09-28)
changeset 2077189bec28a03c8
parent 20770 2c583720436e
child 20772 7a51ed817ec7
proper use of float.ML;
src/HOL/Real/Float.thy
     1.1 --- a/src/HOL/Real/Float.thy	Thu Sep 28 23:42:43 2006 +0200
     1.2 +++ b/src/HOL/Real/Float.thy	Thu Sep 28 23:42:45 2006 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  theory Float
     1.6  imports Real
     1.7 +uses ("float.ML")
     1.8  begin
     1.9  
    1.10  definition
    1.11 @@ -521,4 +522,6 @@
    1.12  (* for use with the compute oracle *)
    1.13  lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
    1.14  
    1.15 +use "float.ML";
    1.16 +
    1.17  end