src/HOL/Library/Library.thy

--- a/src/HOL/Library/Library.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Library/Library.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -8,6 +8,8 @@
   Binomial
   Boolean_Algebra
   Char_ord
+  Code_Index
+  Code_Message
   Coinductive_List
   Commutative_Ring
   Continuity
@@ -18,7 +20,6 @@
   FuncSet
   GCD
   Infinite_Set
-  ML_String
   Multiset
   NatPair
   Nat_Infinity
@@ -27,8 +28,8 @@
   OptionalSugar
   Parity
   Permutation
-  Pretty_Char_chr
-  Pretty_Int
+  Code_Integer
+  Code_Char_chr
   Primes
   Quicksort
   Quotient