--- a/CONTRIBUTORS Sun Jul 12 14:48:01 2009 +0200
+++ b/CONTRIBUTORS Tue Jul 14 10:53:44 2009 +0200
@@ -7,6 +7,12 @@
Contributions to this Isabelle version
--------------------------------------
+* July 2009: Florian Haftmann, TUM
+ New quickcheck implementation using new code generator
+
+* July 2009: Florian Haftmann, TUM
+ HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation
+
* June 2009: Andreas Lochbihler, Uni Karlsruhe
HOL/Library/Fin_Fun: almost everywhere constant functions
--- a/NEWS Sun Jul 12 14:48:01 2009 +0200
+++ b/NEWS Tue Jul 14 10:53:44 2009 +0200
@@ -18,6 +18,16 @@
*** HOL ***
+* Code generator attributes follow the usual underscore convention:
+ code_unfold replaces code unfold
+ code_post replaces code post
+ etc.
+ INCOMPATIBILITY.
+
+* New quickcheck implementation using new code generator.
+
+* New type class boolean_algebra.
+
* Class semiring_div requires superclass no_zero_divisors and proof of
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been