src/HOL/Library/Library.thy

--- a/src/HOL/Library/Library.thy	Wed Dec 03 09:53:58 2008 +0100
+++ b/src/HOL/Library/Library.thy	Wed Dec 03 15:58:44 2008 +0100
@@ -11,7 +11,6 @@
   Code_Char_chr
   Code_Index
   Code_Integer
-  Code_Message
   Coinductive_List
   Commutative_Ring
   Continuity
@@ -21,7 +20,7 @@
   Enum
   Eval_Witness
   Executable_Set
-  "../Real/Float"
+  Float
   FuncSet
   Imperative_HOL
   Infinite_Set