# HG changeset patch
# User wenzelm
# Date 1189970323 -7200
# Node ID 3f238d4987c0aa7899aae5cfd6b3092b8fbced04
# Parent  aae1095dbe3b0d98217f7f8c6053b0c6e55f18c3
tuned;

diff -r aae1095dbe3b -r 3f238d4987c0 src/HOL/Induct/Common_Patterns.thy
--- a/src/HOL/Induct/Common_Patterns.thy	Sun Sep 16 21:04:45 2007 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy	Sun Sep 16 21:18:43 2007 +0200
@@ -354,19 +354,29 @@
 | succ_Evn: "Evn n \<Longrightarrow> Odd (Suc n)"
 | succ_Odd: "Odd n \<Longrightarrow> Evn (Suc n)"
 
-lemma "Evn n \<Longrightarrow> P n"
-  and "Odd n \<Longrightarrow> Q n"
+lemma
+    "Evn n \<Longrightarrow> P1 n"
+    "Evn n \<Longrightarrow> P2 n"
+    "Evn n \<Longrightarrow> P3 n"
+  and
+    "Odd n \<Longrightarrow> Q1 n"
+    "Odd n \<Longrightarrow> Q2 n"
 proof (induct rule: Evn_Odd.inducts)
   case zero
-  show "P 0" sorry
+  { case 1 show "P1 0" sorry }
+  { case 2 show "P2 0" sorry }
+  { case 3 show "P3 0" sorry }
 next
   case (succ_Evn n)
-  note `Evn n` and `P n`
-  show "Q (Suc n)" sorry
+  note `Evn n` and `P1 n` `P2 n` `P3 n`
+  { case 1 show "Q1 (Suc n)" sorry }
+  { case 2 show "Q2 (Suc n)" sorry }
 next
   case (succ_Odd n)
-  note `Odd n` and `Q n`
-  show "P (Suc n)" sorry
+  note `Odd n` and `Q1 n` `Q2 n`
+  { case 1 show "P1 (Suc n)" sorry }
+  { case 2 show "P2 (Suc n)" sorry }
+  { case 3 show "P3 (Suc n)" sorry }
 qed
 
 end
\ No newline at end of file