src/HOL/Library/Library.thy
changeset 51161 6ed12ae3b3e1
parent 50134 13211e07d931
child 51174 071674018df9
--- a/src/HOL/Library/Library.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/Library.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -2,7 +2,7 @@
 theory Library
 imports
   Abstract_Rat
-  AList_Mapping
+  AList
   BigO
   Binomial
   Bit
@@ -29,6 +29,7 @@
   Indicator_Function
   Infinite_Set
   Inner_Product
+  IArray
   Lattice_Algebras
   Lattice_Syntax
   ListVector
@@ -37,7 +38,6 @@
   Monad_Syntax
   Multiset
   Numeral_Type
-  Old_Recdef
   OptionalSugar
   Option_ord
   Parallel
@@ -56,11 +56,10 @@
   Quotient_Type
   Ramsey
   Reflection
-  RBT_Mapping
-  (* RBT_Set *) (* FIXME not included because it breaks Codegenerator_Test/Generate*.thy *)
   Saturated
   Set_Algebras
   State_Monad
+  Sublist
   Sum_of_Squares
   Transitive_Closure_Table
   Univ_Poly