# HG changeset patch
# User haftmann
# Date 1282048419 -7200
# Node ID 75fc4087764eaf7234b04696d7f2159cfbd3b850
# Parent  628fee3eb449222ea9d1502b10d1fa96557e8032
NEWS and CONTRIBUTORS

diff -r 628fee3eb449 -r 75fc4087764e CONTRIBUTORS
--- 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
 --------------------------------------
diff -r 628fee3eb449 -r 75fc4087764e NEWS
--- 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 ***