--- a/CONTRIBUTORS Tue Aug 17 14:19:12 2010 +0200
+++ b/CONTRIBUTORS Tue Aug 17 14:33:39 2010 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* July 2010: Florian Haftmann, TUM
+ Reworking and extension of the Isabelle/HOL framework.
+
Contributions to Isabelle2009-2
--------------------------------------
--- a/NEWS Tue Aug 17 14:19:12 2010 +0200
+++ b/NEWS Tue Aug 17 14:33:39 2010 +0200
@@ -35,11 +35,17 @@
*** HOL ***
+* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
+INCOMPATIBILITY.
+
+* Quickcheck in locales considers interpretations of that locale for
+counter example search.
+
* Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax
in Library/State_Monad has been changed to avoid ambiguities.
INCOMPATIBILITY.
-* code generator: export_code without explicit file declaration prints
+* Code generator: export_code without explicit file declaration prints
to standard output. INCOMPATIBILITY.
* Abolished symbol type names: "prod" and "sum" replace "*" and "+"
@@ -121,8 +127,8 @@
INCOMPATIBILITY.
* Inductive package: offers new command "inductive_simps" to automatically
- derive instantiated and simplified equations for inductive predicates,
- similar to inductive_cases.
+derive instantiated and simplified equations for inductive predicates,
+similar to inductive_cases.
*** ML ***