author | blanchet |
Thu, 19 Sep 2013 18:59:28 +0200 | |
changeset 53738 | 9868e6d4733f |
parent 53737 | eab25a77af39 |
child 53739 | 599d8c324477 |
--- a/NEWS Thu Sep 19 18:03:54 2013 +0200 +++ b/NEWS Thu Sep 19 18:59:28 2013 +0200 @@ -388,9 +388,13 @@ INCOMPATIBILITY. +* Nitpick: + - Reduce incidence of "too high arity" errors + * Sledgehammer: - Renamed option: isar_shrink ~> isar_compress + INCOMPATIBILITY. - Better support for "isar_proofs" * Imperative-HOL: The MREC combinator is considered legacy and no