# HG changeset patch
# User wenzelm
# Date 1435653642 -7200
# Node ID 0eb41780449bf9e6a285c5df42d7e64b991d551b
# Parent  79d71bfea3105ce0925fbebf299a4f25f6dabd30
tuned;

diff -r 79d71bfea310 -r 0eb41780449b NEWS
--- a/NEWS	Mon Jun 29 23:44:53 2015 +0200
+++ b/NEWS	Tue Jun 30 10:40:42 2015 +0200
@@ -99,10 +99,22 @@
 
 * Proof method "goals" turns the current subgoals into cases within the
 context; the conclusion is bound to variable ?case in each case.
+For example:
+
+lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
+  and "\<And>y z. U y \<Longrightarrow> V u \<Longrightarrow> W y z"
+proof goals
+  case prems: 1
+  then show ?case using prems sorry
+next
+  case prems: 2
+  then show ?case using prems sorry
+qed
 
 * The undocumented feature of implicit cases goal1, goal2, goal3, etc.
-is marked as legacy, and will be removed eventually. Note that proof
-method "goals" achieves a similar effect within regular Isar.
+is marked as legacy, and will be removed eventually. The proof method
+"goals" achieves a similar effect within regular Isar; often it can be
+done more adequately by other means (e.g. 'consider').
 
 * Nesting of Isar goal structure has been clarified: the context after
 the initial backwards refinement is retained for the whole proof, within