--- 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