--- a/NEWS Mon Jun 22 11:35:30 2015 +0200
+++ b/NEWS Mon Jun 22 16:48:27 2015 +0200
@@ -62,6 +62,19 @@
then show ?thesis <proof>
qed
+* 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.
+relevant for 'using', 'including', 'supply':
+
+ have "A \<and> A" if a: A for A
+ supply [simp] = a
+ proof
+ show A by simp
+ next
+ show A by simp
+ qed
+
*** Pure ***