# HG changeset patch
# User wenzelm
# Date 1404466774 -7200
# Node ID 3e04e25a751e0db87db1fd7e5bc7d99a378a0ab0
# Parent  2cfefeee7bba33dcfda2db7e02e187bdcd07541a
NEWS;

diff -r 2cfefeee7bba -r 3e04e25a751e NEWS
--- a/NEWS	Thu Jul 03 16:42:15 2014 +0200
+++ b/NEWS	Fri Jul 04 11:39:34 2014 +0200
@@ -51,6 +51,18 @@
 * Updated and extended manuals: codegen, datatypes, implementation,
 isar-ref, jedit, system.
 
+* Standard tactics and proof methods such as "clarsimp", "auto" and
+"safe" now preserve equality hypotheses "x = expr" where x is a free
+variable.  Locale assumptions and chained facts containing "x"
+continue to be useful.  The new method "hypsubst_thin" and the
+configuration option "hypsubst_thin" (within the attribute name space)
+restore the previous behavior.
+
+INCOMPATIBILITY, especially where induction is done after these
+methods or when the names of free and bound variables clash.  As first
+approximation, old proofs may be repaired by "using [[hypsubst_thin =
+true]]" in the critical spot.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***