diff -r a75d71c73362 -r 9f90ac19e32b src/HOL/Library/Library.thy --- 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 (*>*)