src/HOL/Matrix/ComputeFloat.thy
changeset 35032 7efe662e41b4
parent 32491 d5d8bea0cd94
child 38273 d31a34569542
     1.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Fri Feb 05 14:33:50 2010 +0100
     1.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Mon Feb 08 14:06:41 2010 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Floating Point Representation of the Reals *}
     1.5  
     1.6  theory ComputeFloat
     1.7 -imports Complex_Main
     1.8 +imports Complex_Main Lattice_Algebras
     1.9  uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
    1.10  begin
    1.11