add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
authorhuffman
Thu, 03 Jul 2008 18:16:40 +0200
changeset 27475 61b979a2c820
parent 27474 a89d755b029d
child 27476 964766deef47
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu Jul 03 18:15:39 2008 +0200
+++ b/src/HOL/Library/Library.thy	Thu Jul 03 18:16:40 2008 +0200
@@ -24,6 +24,7 @@
   "../Real/Float"
   FuncSet
   Imperative_HOL
+  Infinite_Set
   ListVector
   Multiset
   NatPair
@@ -41,6 +42,7 @@
   State_Monad
   While_Combinator
   Word
+  Zorn
 begin
 end
 (*>*)