2015-06-17 nipkow [Wed, 17 Jun 2015 18:13:44 +0200] rev 60498
more compact name
src/HOL/Library/Multiset.thy

2015-06-17 nipkow [Wed, 17 Jun 2015 17:33:22 +0200] rev 60497
NEWS
NEWS

2015-06-17 nipkow [Wed, 17 Jun 2015 17:21:20 +0200] rev 60496
merged

2015-06-17 nipkow [Wed, 17 Jun 2015 17:21:11 +0200] rev 60495
renamed Multiset.set_of to the canonical set_mset
src/HOL/Algebra/Divisibility.thy src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy src/HOL/Library/DAList_Multiset.thy src/HOL/Library/Multiset.thy src/HOL/Library/Multiset_Order.thy src/HOL/Library/Permutation.thy src/HOL/Library/Tree_Multiset.thy src/HOL/Number_Theory/UniqueFactorization.thy src/HOL/Probability/Probability_Mass_Function.thy src/HOL/ZF/LProd.thy

2015-06-17 paulson <lp15@cam.ac.uk> [Wed, 17 Jun 2015 15:15:52 +0100] rev 60494
correccted the pretty-printing specs for setsum and setprod
src/HOL/Groups_Big.thy

2015-06-17 paulson <lp15@cam.ac.uk> [Wed, 17 Jun 2015 14:35:50 +0100] rev 60493
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
src/HOL/Wellfounded.thy

2015-06-16 paulson <lp15@cam.ac.uk> [Tue, 16 Jun 2015 20:50:00 +0100] rev 60492
another messy proof fixed
src/HOL/Multivariate_Analysis/Integration.thy

2015-06-15 wenzelm [Mon, 15 Jun 2015 23:56:40 +0200] rev 60491
merged

2015-06-15 wenzelm [Mon, 15 Jun 2015 17:29:43 +0200] rev 60490
more informative check: dummies are always allowed parse_term and should not lead to rejection here;
src/Pure/Syntax/syntax_phases.ML

2015-06-15 wenzelm [Mon, 15 Jun 2015 16:59:27 +0200] rev 60489
vacuous fact `TERM x`;
NEWS src/Pure/Isar/proof_context.ML