--- a/NEWS Thu Jun 18 09:07:54 2020 +0000
+++ b/NEWS Fri Jun 19 09:46:47 2020 +0000
@@ -64,15 +64,21 @@
"bintrunc" and "max_word" are now mere input abbreviations.
Minor INCOMPATIBILITY.
+* Rewrite rule subst_all performs
+more aggressive substitution with variables from assumptions.
+INCOMPATIBILITY, use something like
+"supply subst_all [simp del]"
+to leave fragile proofs unaffected.
+
*** FOL ***
* Added the "at most 1" quantifier, Uniq, as in HOL.
-* Simproc defined_all and rewrite rules subst_all and subst_all' perform
+* Simproc defined_all and rewrite rule 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]]"
+"supply subst_all [simp del] [[simproc del: defined_all]]"
to leave fragile proofs unaffected.