src/HOL/Library/Library.thy
changeset 43919 a7e4fb1a0502
parent 43241 93b1183e43e5
child 43958 bc5e767f0f46
--- a/src/HOL/Library/Library.thy	Tue Jul 19 11:15:38 2011 +0200
+++ b/src/HOL/Library/Library.thy	Tue Jul 19 14:35:44 2011 +0200
@@ -15,6 +15,7 @@
   Diagonalize
   Dlist_Cset
   Eval_Witness
+  Extended_Nat
   Float
   Formal_Power_Series
   Fraction_Field
@@ -35,7 +36,6 @@
   Monad_Syntax
   More_List
   Multiset
-  Nat_Infinity
   Nested_Environment
   Numeral_Type
   OptionalSugar