--- a/NEWS Thu Jun 25 16:56:04 2015 +0200
+++ b/NEWS Thu Jun 25 21:45:00 2015 +0200
@@ -77,6 +77,9 @@
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
and always put attributes in front.
+* Proof method "goals" turns the current subgoals into cases within the
+context; the conclusion is bound to variable ?case in each case.
+
* Nesting of Isar goal structure has been clarified: the context after
the initial backwards refinement is retained for the whole proof, within
all its context sections (as indicated via 'next'). This is e.g.