src/HOL/Library/Library.thy
changeset 30240 5b25fee0362c
parent 29879 4425849f5db7
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Library/Library.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Library/Library.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -5,6 +5,7 @@
     1.4    AssocList
     1.5    BigO
     1.6    Binomial
     1.7 +  Bit
     1.8    Boolean_Algebra
     1.9    Char_ord
    1.10    Code_Char_chr
    1.11 @@ -22,9 +23,11 @@
    1.12    Executable_Set
    1.13    Float
    1.14    Formal_Power_Series
    1.15 +  FrechetDeriv
    1.16    FuncSet
    1.17    Fundamental_Theorem_Algebra
    1.18    Infinite_Set
    1.19 +  Inner_Product
    1.20    ListVector
    1.21    Mapping
    1.22    Multiset
    1.23 @@ -35,7 +38,10 @@
    1.24    Option_ord
    1.25    Permutation
    1.26    Pocklington
    1.27 +  Poly_Deriv
    1.28 +  Polynomial
    1.29    Primes
    1.30 +  Product_Vector
    1.31    Quickcheck
    1.32    Quicksort
    1.33    Quotient