NEWS

--- a/NEWS	Thu Jun 04 19:38:52 2020 +0000
+++ b/NEWS	Sat Jun 06 10:58:13 2020 +0200
@@ -40,6 +40,12 @@
 
 * Added the "at most 1" quantifier, Uniq, as in HOL.
 
+* Simproc defined_all and rewrite rules subst_all and subst_all' perform
+more aggressive substitution with variables from assumptions.
+INCOMPATIBILITY, use something like
+"supply subst_all [simp] subst_all' [simp] [[simproc del: defined_all]]"
+to leave fragile proofs unaffected.
+
 
 *** ML ***