diff -r 179ff9cb160b -r 5b25fee0362c src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Library/Library.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -5,6 +5,7 @@
   AssocList
   BigO
   Binomial
+  Bit
   Boolean_Algebra
   Char_ord
   Code_Char_chr
@@ -22,9 +23,11 @@
   Executable_Set
   Float
   Formal_Power_Series
+  FrechetDeriv
   FuncSet
   Fundamental_Theorem_Algebra
   Infinite_Set
+  Inner_Product
   ListVector
   Mapping
   Multiset
@@ -35,7 +38,10 @@
   Option_ord
   Permutation
   Pocklington
+  Poly_Deriv
+  Polynomial
   Primes
+  Product_Vector
   Quickcheck
   Quicksort
   Quotient