diff -r b3ae84c6e509 -r a01b2de0e3e1 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Mar 06 20:29:37 2009 +0100
+++ b/src/HOL/Library/Library.thy	Fri Mar 06 20:30:16 2009 +0100
@@ -17,6 +17,7 @@
   ContNotDenum
   Countable
   Determinants
+  Diagonalize
   Efficient_Nat
   Enum
   Eval_Witness
@@ -28,6 +29,7 @@
   Fundamental_Theorem_Algebra
   Infinite_Set
   Inner_Product
+  Lattice_Syntax
   ListVector
   Mapping
   Multiset