changeset 57503 3e04e25a751e
parent 57491 9eedaafc05c8
child 57504 5cf245c62c4c
--- 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 ***