src/HOL/Complex/ex/MIR.thy

--- a/src/HOL/Complex/ex/MIR.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -5,7 +5,7 @@
 header {* Quatifier elimination for R(0,1,+,floor,<) *}
 
 theory MIR
-  imports Real GCD Pretty_Int
+  imports Real GCD Code_Integer
   uses ("mireif.ML") ("mirtac.ML")
   begin