# HG changeset patch
# User wenzelm
# Date 1435740794 -7200
# Node ID 57b5293bceacc38d2ff9d1ec5d5e845e8dc28aa8
# Parent  41e180848d021b0158442eeffabaa0ef3283ee2a
tuned;

diff -r 41e180848d02 -r 57b5293bceac NEWS
--- a/NEWS	Tue Jun 30 17:02:24 2015 +0200
+++ b/NEWS	Wed Jul 01 10:53:14 2015 +0200
@@ -107,7 +107,17 @@
 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"
+  and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
+proof goals
+  case (1 x)
+  then show ?case using \<open>A x\<close> \<open>B x\<close> sorry
+next
+  case (2 y z)
+  then show ?case using \<open>U y\<close> \<open>V z\<close> sorry
+qed
+
+lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
+  and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
 proof goals
   case prems: 1
   then show ?case using prems sorry