2011-12-20 noschinl [Tue, 20 Dec 2011 11:40:56 +0100] rev 45934
add simp rules for enat and ereal
src/HOL/Library/Extended_Nat.thy src/HOL/Library/Extended_Real.thy src/HOL/Probability/Probability_Measure.thy

2011-12-19 noschinl [Mon, 19 Dec 2011 14:41:08 +0100] rev 45933
add lemmas
src/HOL/Nat.thy src/HOL/Number_Theory/Binomial.thy

2011-12-19 noschinl [Mon, 19 Dec 2011 14:41:08 +0100] rev 45932
add lemmas
src/HOL/List.thy src/HOL/SetInterval.thy

2011-12-19 noschinl [Mon, 19 Dec 2011 14:41:08 +0100] rev 45931
weaken preconditions on lemmas
src/HOL/Nat.thy src/HOL/Orderings.thy

2011-12-19 noschinl [Mon, 19 Dec 2011 14:41:08 +0100] rev 45930
add lemmas
src/HOL/Fact.thy src/HOL/Log.thy

2011-12-20 bulwahn [Tue, 20 Dec 2011 17:40:21 +0100] rev 45929
removing some debug output in quotient_definition
src/HOL/Tools/Quotient/quotient_def.ML

2011-12-20 bulwahn [Tue, 20 Dec 2011 17:40:18 +0100] rev 45928
adding quickcheck generators in some HOL-Library theories
src/HOL/Library/Polynomial.thy src/HOL/Library/RBT.thy

2011-12-20 bulwahn [Tue, 20 Dec 2011 17:40:17 +0100] rev 45927
adding quickcheck generator for distinct lists; adding examples
src/HOL/Library/Dlist.thy src/HOL/ex/Quickcheck_Examples.thy

2011-12-20 bulwahn [Tue, 20 Dec 2011 17:40:15 +0100] rev 45926
added keywords
etc/isar-keywords.el

2011-12-20 bulwahn [Tue, 20 Dec 2011 17:39:56 +0100] rev 45925
quickcheck generators for abstract types; tuned
src/HOL/Quickcheck_Exhaustive.thy src/HOL/Tools/Quickcheck/abstract_generators.ML