src/HOL/Library/Library.thy
changeset 51161 6ed12ae3b3e1
parent 50134 13211e07d931
child 51174 071674018df9
     1.1 --- a/src/HOL/Library/Library.thy	Fri Feb 15 11:47:33 2013 +0100
     1.2 +++ b/src/HOL/Library/Library.thy	Fri Feb 15 11:47:34 2013 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  theory Library
     1.5  imports
     1.6    Abstract_Rat
     1.7 -  AList_Mapping
     1.8 +  AList
     1.9    BigO
    1.10    Binomial
    1.11    Bit
    1.12 @@ -29,6 +29,7 @@
    1.13    Indicator_Function
    1.14    Infinite_Set
    1.15    Inner_Product
    1.16 +  IArray
    1.17    Lattice_Algebras
    1.18    Lattice_Syntax
    1.19    ListVector
    1.20 @@ -37,7 +38,6 @@
    1.21    Monad_Syntax
    1.22    Multiset
    1.23    Numeral_Type
    1.24 -  Old_Recdef
    1.25    OptionalSugar
    1.26    Option_ord
    1.27    Parallel
    1.28 @@ -56,11 +56,10 @@
    1.29    Quotient_Type
    1.30    Ramsey
    1.31    Reflection
    1.32 -  RBT_Mapping
    1.33 -  (* RBT_Set *) (* FIXME not included because it breaks Codegenerator_Test/Generate*.thy *)
    1.34    Saturated
    1.35    Set_Algebras
    1.36    State_Monad
    1.37 +  Sublist
    1.38    Sum_of_Squares
    1.39    Transitive_Closure_Table
    1.40    Univ_Poly