diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Wed Nov 08 22:24:54 2006 +0100
+++ b/src/HOL/Real/Float.thy	Wed Nov 08 23:11:13 2006 +0100
@@ -6,7 +6,7 @@
 header {* Floating Point Representation of the Reals *}
 
 theory Float
-imports Real
+imports Real Parity
 uses ("float.ML")
 begin