--- a/NEWS Wed Aug 10 09:33:54 2016 +0200
+++ b/NEWS Wed Aug 10 15:42:52 2016 +0200
@@ -49,6 +49,14 @@
context. Unlike "context includes ... begin", the effect of 'unbundle'
on the target context persists, until different declarations are given.
+* Splitter in simp, auto and friends:
+- The syntax "split add" has been discontinued, use plain "split".
+- For situations with many nested conditional or case expressions,
+there is an alternative splitting strategy that can be much faster.
+It is selected by writing "split!" instead of "split". It applies
+safe introduction and elimination rules after each split rule.
+As a result the subgoal may be split into several subgoals.
+
* Proof method "blast" is more robust wrt. corner cases of Pure
statements without object-logic judgment.