src/HOL/Library/Library.thy
changeset 24994 c385c4eabb3b
parent 24626 85eceef2edc7
child 25315 6ff4305d2f7c
     1.1 --- a/src/HOL/Library/Library.thy	Fri Oct 12 08:20:46 2007 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Fri Oct 12 08:21:09 2007 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4    Binomial
     1.5    Boolean_Algebra
     1.6    Char_ord
     1.7 +  Code_Index
     1.8 +  Code_Message
     1.9    Coinductive_List
    1.10    Commutative_Ring
    1.11    Continuity
    1.12 @@ -18,7 +20,6 @@
    1.13    FuncSet
    1.14    GCD
    1.15    Infinite_Set
    1.16 -  ML_String
    1.17    Multiset
    1.18    NatPair
    1.19    Nat_Infinity
    1.20 @@ -27,8 +28,8 @@
    1.21    OptionalSugar
    1.22    Parity
    1.23    Permutation
    1.24 -  Pretty_Char_chr
    1.25 -  Pretty_Int
    1.26 +  Code_Integer
    1.27 +  Code_Char_chr
    1.28    Primes
    1.29    Quicksort
    1.30    Quotient