# HG changeset patch
# User huffman
# Date 1215101800 -7200
# Node ID 61b979a2c8209cd7a1f43d96280960b3f3394bea
# Parent  a89d755b029d010f5ed476c33a2b72d3d8df029b
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)

diff -r a89d755b029d -r 61b979a2c820 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
 (*>*)