src/HOL/Library/Library.thy

--- a/src/HOL/Library/Library.thy	Wed Feb 27 21:41:07 2008 +0100
+++ b/src/HOL/Library/Library.thy	Wed Feb 27 21:41:08 2008 +0100
@@ -8,18 +8,22 @@
   Binomial
   Boolean_Algebra
   Char_ord
+  Code_Char_chr
   Code_Index
+  Code_Integer
   Code_Message
   Coinductive_List
   Commutative_Ring
   Continuity
+  Countable
   Dense_Linear_Order
   Efficient_Nat
-  (*Eval*)
+  Eval
   Eval_Witness
   Executable_Set
   FuncSet
   GCD
+  Imperative_HOL
   Infinite_Set
   ListSpace
   Multiset
@@ -30,8 +34,6 @@
   OptionalSugar
   Parity
   Permutation
-  Code_Integer
-  Code_Char_chr
   Primes
   Quicksort
   Quotient