2011-12-27 haftmann [Tue, 27 Dec 2011 09:45:10 +0100] rev 45994
be explicit about Finite_Set.fold
src/HOL/Library/Saturated.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Quotient_Examples/FSet.thy

2011-12-27 haftmann [Tue, 27 Dec 2011 09:15:26 +0100] rev 45993
dropped fact whose names clash with corresponding facts on canonical fold
src/HOL/List.thy src/HOL/More_List.thy

2011-12-27 haftmann [Tue, 27 Dec 2011 09:15:26 +0100] rev 45992
prefer canonical fold on lists
src/HOL/GCD.thy

2011-12-27 haftmann [Tue, 27 Dec 2011 09:15:26 +0100] rev 45991
be explicit about Finite_Set.fold
NEWS

2011-12-26 haftmann [Mon, 26 Dec 2011 22:17:10 +0100] rev 45990
incorporated More_Set and More_List into the Main body -- to be consolidated later
src/HOL/IMP/Abs_Int1_ivl.thy src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy src/HOL/IsaMakefile src/HOL/Library/AList_Impl.thy src/HOL/Library/Cset.thy src/HOL/Library/Dlist.thy src/HOL/Library/Library.thy src/HOL/Library/Monad_Syntax.thy src/HOL/Library/More_List.thy src/HOL/Library/More_Set.thy src/HOL/Library/RBT_Impl.thy src/HOL/Main.thy src/HOL/MicroJava/BV/BVExample.thy src/HOL/More_List.thy src/HOL/More_Set.thy src/HOL/Quotient_Examples/DList.thy src/HOL/Quotient_Examples/FSet.thy src/HOL/Quotient_Examples/Quotient_Cset.thy src/HOL/ex/Quickcheck_Examples.thy

2011-12-26 haftmann [Mon, 26 Dec 2011 22:17:10 +0100] rev 45989
moved theorem requiring multisets from More_List to Multiset
src/HOL/Library/Multiset.thy

2011-12-26 haftmann [Mon, 26 Dec 2011 22:17:10 +0100] rev 45988
NEWS: unavoidable fact renames
NEWS

2011-12-26 haftmann [Mon, 26 Dec 2011 18:32:43 +0100] rev 45987
dropped disfruitful `constant signatures`
src/Pure/Isar/code.ML src/Tools/Code/code_thingol.ML

2011-12-26 haftmann [Mon, 26 Dec 2011 18:32:43 +0100] rev 45986
moved various set operations to theory Set (resp. Product_Type)
src/HOL/Library/Cset.thy src/HOL/Library/More_Set.thy src/HOL/MicroJava/BV/BVExample.thy src/HOL/Product_Type.thy src/HOL/Quotient_Examples/List_Quotient_Cset.thy src/HOL/Quotient_Examples/Quotient_Cset.thy src/HOL/Set.thy

2011-12-26 haftmann [Mon, 26 Dec 2011 17:40:43 +0100] rev 45985
dropped Executable_Set wrapper theory
src/HOL/IsaMakefile src/HOL/Library/Executable_Set.thy src/HOL/Library/ROOT.ML src/HOL/MicroJava/BV/BVExample.thy