1.1 --- a/src/HOL/Induct/Common_Patterns.thy	Sun Sep 16 21:04:45 2007 +0200
     1.2 +++ b/src/HOL/Induct/Common_Patterns.thy	Sun Sep 16 21:18:43 2007 +0200
     1.3 @@ -354,19 +354,29 @@
     1.4  | succ_Evn: "Evn n \<Longrightarrow> Odd (Suc n)"
     1.5  | succ_Odd: "Odd n \<Longrightarrow> Evn (Suc n)"
     1.6  
     1.7 -lemma "Evn n \<Longrightarrow> P n"
     1.8 -  and "Odd n \<Longrightarrow> Q n"
     1.9 +lemma
    1.10 +    "Evn n \<Longrightarrow> P1 n"
    1.11 +    "Evn n \<Longrightarrow> P2 n"
    1.12 +    "Evn n \<Longrightarrow> P3 n"
    1.13 +  and
    1.14 +    "Odd n \<Longrightarrow> Q1 n"
    1.15 +    "Odd n \<Longrightarrow> Q2 n"
    1.16  proof (induct rule: Evn_Odd.inducts)
    1.17    case zero
    1.18 -  show "P 0" sorry
    1.19 +  { case 1 show "P1 0" sorry }
    1.20 +  { case 2 show "P2 0" sorry }
    1.21 +  { case 3 show "P3 0" sorry }
    1.22  next
    1.23    case (succ_Evn n)
    1.24 -  note `Evn n` and `P n`
    1.25 -  show "Q (Suc n)" sorry
    1.26 +  note `Evn n` and `P1 n` `P2 n` `P3 n`
    1.27 +  { case 1 show "Q1 (Suc n)" sorry }
    1.28 +  { case 2 show "Q2 (Suc n)" sorry }
    1.29  next
    1.30    case (succ_Odd n)
    1.31 -  note `Odd n` and `Q n`
    1.32 -  show "P (Suc n)" sorry
    1.33 +  note `Odd n` and `Q1 n` `Q2 n`
    1.34 +  { case 1 show "P1 (Suc n)" sorry }
    1.35 +  { case 2 show "P2 (Suc n)" sorry }
    1.36 +  { case 3 show "P3 (Suc n)" sorry }
    1.37  qed
    1.38  
    1.39  end
    1.40 \ No newline at end of file