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