src/HOL/Library/Library.thy
changeset 27368 9f90ac19e32b
parent 27298 a5373b60e66c
child 27475 61b979a2c820
--- a/src/HOL/Library/Library.thy	Thu Jun 26 10:06:54 2008 +0200
+++ b/src/HOL/Library/Library.thy	Thu Jun 26 10:07:01 2008 +0200
@@ -2,7 +2,6 @@
 (*<*)
 theory Library
 imports
-  Abstract_Rat
   AssocList
   BigO
   Binomial
@@ -24,9 +23,7 @@
   Executable_Set
   "../Real/Float"
   FuncSet
-  GCD
   Imperative_HOL
-  Infinite_Set
   ListVector
   Multiset
   NatPair
@@ -35,8 +32,6 @@
   Numeral_Type
   OptionalSugar
   Option_ord
-  Order_Relation
-  Parity
   Permutation
   Primes
   Quicksort
@@ -44,10 +39,8 @@
   Ramsey
   RBT
   State_Monad
-  Univ_Poly
   While_Combinator
   Word
-  Zorn
 begin
 end
 (*>*)