src/HOL/Library/Library.thy
changeset 26170 66e6b967ccf1
parent 26157 4d9d0a26c32a
child 26173 5cac519abe4e
     1.1 --- a/src/HOL/Library/Library.thy	Wed Feb 27 21:41:07 2008 +0100
     1.2 +++ b/src/HOL/Library/Library.thy	Wed Feb 27 21:41:08 2008 +0100
     1.3 @@ -8,18 +8,22 @@
     1.4    Binomial
     1.5    Boolean_Algebra
     1.6    Char_ord
     1.7 +  Code_Char_chr
     1.8    Code_Index
     1.9 +  Code_Integer
    1.10    Code_Message
    1.11    Coinductive_List
    1.12    Commutative_Ring
    1.13    Continuity
    1.14 +  Countable
    1.15    Dense_Linear_Order
    1.16    Efficient_Nat
    1.17 -  (*Eval*)
    1.18 +  Eval
    1.19    Eval_Witness
    1.20    Executable_Set
    1.21    FuncSet
    1.22    GCD
    1.23 +  Imperative_HOL
    1.24    Infinite_Set
    1.25    ListSpace
    1.26    Multiset
    1.27 @@ -30,8 +34,6 @@
    1.28    OptionalSugar
    1.29    Parity
    1.30    Permutation
    1.31 -  Code_Integer
    1.32 -  Code_Char_chr
    1.33    Primes
    1.34    Quicksort
    1.35    Quotient