Quotient_Set.thy is part of library
authorhaftmann
Sun, 25 Sep 2011 09:37:33 +0200
changeset 4594504286b0fc856
parent 45944 9bcbdf987601
child 45946 6c66e268f8eb
Quotient_Set.thy is part of library
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/IsaMakefile	Sun Sep 25 00:32:49 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sun Sep 25 09:37:33 2011 +0200
     1.3 @@ -464,10 +464,11 @@
     1.4    Library/Product_plus.thy Library/Product_Lattice.thy			\
     1.5    Library/Quickcheck_Types.thy Library/Quotient_List.thy		\
     1.6    Library/Quotient_Option.thy Library/Quotient_Product.thy		\
     1.7 -  Library/Quotient_Sum.thy Library/Quotient_Syntax.thy			\
     1.8 -  Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy	\
     1.9 -  Library/RBT_Mapping.thy Library/README.html Library/Saturated.thy	\
    1.10 -  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
    1.11 +  Library/Quotient_Set.thy Library/Quotient_Sum.thy			\
    1.12 +  Library/Quotient_Syntax.thy Library/Quotient_Type.thy Library/RBT.thy	\
    1.13 +  Library/RBT_Impl.thy Library/RBT_Mapping.thy Library/README.html	\
    1.14 +  Library/Saturated.thy Library/Set_Algebras.thy			\
    1.15 +  Library/State_Monad.thy Library/Ramsey.thy				\
    1.16    Library/Reflection.thy Library/Sublist_Order.thy			\
    1.17    Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML	\
    1.18    Library/Sum_of_Squares/sum_of_squares.ML				\
     2.1 --- a/src/HOL/Library/Library.thy	Sun Sep 25 00:32:49 2011 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Sun Sep 25 09:37:33 2011 +0200
     2.3 @@ -49,6 +49,7 @@
     2.4    Quotient_List
     2.5    Quotient_Option
     2.6    Quotient_Product
     2.7 +  Quotient_Set
     2.8    Quotient_Sum
     2.9    Quotient_Syntax
    2.10    Quotient_Type