src/HOL/Library/Library.thy
changeset 27368 9f90ac19e32b
parent 27298 a5373b60e66c
child 27475 61b979a2c820
     1.1 --- a/src/HOL/Library/Library.thy	Thu Jun 26 10:06:54 2008 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Thu Jun 26 10:07:01 2008 +0200
     1.3 @@ -2,7 +2,6 @@
     1.4  (*<*)
     1.5  theory Library
     1.6  imports
     1.7 -  Abstract_Rat
     1.8    AssocList
     1.9    BigO
    1.10    Binomial
    1.11 @@ -24,9 +23,7 @@
    1.12    Executable_Set
    1.13    "../Real/Float"
    1.14    FuncSet
    1.15 -  GCD
    1.16    Imperative_HOL
    1.17 -  Infinite_Set
    1.18    ListVector
    1.19    Multiset
    1.20    NatPair
    1.21 @@ -35,8 +32,6 @@
    1.22    Numeral_Type
    1.23    OptionalSugar
    1.24    Option_ord
    1.25 -  Order_Relation
    1.26 -  Parity
    1.27    Permutation
    1.28    Primes
    1.29    Quicksort
    1.30 @@ -44,10 +39,8 @@
    1.31    Ramsey
    1.32    RBT
    1.33    State_Monad
    1.34 -  Univ_Poly
    1.35    While_Combinator
    1.36    Word
    1.37 -  Zorn
    1.38  begin
    1.39  end
    1.40  (*>*)