| changeset 71923 | 7b34a932eeb6 |
| parent 71909 | cdcf2fcf3f54 |
| child 71924 | e5df9c8d9d4b |
--- 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 ***