# HG changeset patch
# User haftmann
# Date 1316936253 -7200
# Node ID 04286b0fc856ea831a6bb860b198576eb01493b0
# Parent  9bcbdf9876015aef73cb0ed132804381018ff202
Quotient_Set.thy is part of library

diff -r 9bcbdf987601 -r 04286b0fc856 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Sep 25 00:32:49 2011 +0200
+++ b/src/HOL/IsaMakefile	Sun Sep 25 09:37:33 2011 +0200
@@ -464,10 +464,11 @@
   Library/Product_plus.thy Library/Product_Lattice.thy			\
   Library/Quickcheck_Types.thy Library/Quotient_List.thy		\
   Library/Quotient_Option.thy Library/Quotient_Product.thy		\
-  Library/Quotient_Sum.thy Library/Quotient_Syntax.thy			\
-  Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy	\
-  Library/RBT_Mapping.thy Library/README.html Library/Saturated.thy	\
-  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
+  Library/Quotient_Set.thy Library/Quotient_Sum.thy			\
+  Library/Quotient_Syntax.thy Library/Quotient_Type.thy Library/RBT.thy	\
+  Library/RBT_Impl.thy Library/RBT_Mapping.thy Library/README.html	\
+  Library/Saturated.thy Library/Set_Algebras.thy			\
+  Library/State_Monad.thy Library/Ramsey.thy				\
   Library/Reflection.thy Library/Sublist_Order.thy			\
   Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML	\
   Library/Sum_of_Squares/sum_of_squares.ML				\
diff -r 9bcbdf987601 -r 04286b0fc856 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Sun Sep 25 00:32:49 2011 +0200
+++ b/src/HOL/Library/Library.thy	Sun Sep 25 09:37:33 2011 +0200
@@ -49,6 +49,7 @@
   Quotient_List
   Quotient_Option
   Quotient_Product
+  Quotient_Set
   Quotient_Sum
   Quotient_Syntax
   Quotient_Type