NEWS

--- a/NEWS	Thu Jul 02 08:49:04 2020 +0000
+++ b/NEWS	Thu Jul 02 12:10:58 2020 +0000
@@ -77,10 +77,10 @@
 * Session HOL-Word: Theory Z2 is not used any longer.
 Minor INCOMPATIBILITY.
 
-* Rewrite rule subst_all performs
+* Simproc defined_all and rewrite rule subst_all perform
 more aggressive substitution with variables from assumptions.
 INCOMPATIBILITY, use something like
-"supply subst_all [simp del]"
+"supply subst_all [simp del] [[simproc del: defined_all]]"
 to leave fragile proofs unaffected.