src/HOL/Library/Library.thy
changeset 43919 a7e4fb1a0502
parent 43241 93b1183e43e5
child 43958 bc5e767f0f46
     1.1 --- a/src/HOL/Library/Library.thy	Tue Jul 19 11:15:38 2011 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Tue Jul 19 14:35:44 2011 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    Diagonalize
     1.5    Dlist_Cset
     1.6    Eval_Witness
     1.7 +  Extended_Nat
     1.8    Float
     1.9    Formal_Power_Series
    1.10    Fraction_Field
    1.11 @@ -35,7 +36,6 @@
    1.12    Monad_Syntax
    1.13    More_List
    1.14    Multiset
    1.15 -  Nat_Infinity
    1.16    Nested_Environment
    1.17    Numeral_Type
    1.18    OptionalSugar