NEWS
changeset 60622 57b5293bceac
parent 60618 4c79543cc376
child 60631 441fdbfbb2d3
--- 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