--- a/NEWS Wed Jun 24 00:30:03 2015 +0200
+++ b/NEWS Wed Jun 24 21:26:03 2015 +0200
@@ -66,6 +66,17 @@
then show ?thesis <proof>
qed
+* Command 'case' allows fact name and attribute specification like this:
+
+ case a: (c xs)
+ case a [attributes]: (c xs)
+
+Facts that are introduced by invoking the case context are uniformly
+qualified by "a"; the same name is used for the cumulative fact. The old
+form "case (c xs) [attributes]" is no longer supported. Rare
+INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
+and always put attributes in front.
+
* 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.