--- 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