# [isabelle] [Isabelle2016-1-RC2] Proof outlines for induction proofs with several simultaneous goals

Dear Makarius,

`Thanks for implementing proof outlines in Isabelle2016-1-RC2. I really find them useful.
``Unfortunately, they are not yet right for induction proofs with several goals. Here's a
``small example:
`
lemma
fixes xs :: "'a list"
shows "xs = xs" "xs @ xs = xs @ xs"
proof(induction xs)
The suggested proof outline is
case Nil
then show ?thesis sorry
next
case (Cons a xs)
then show ?thesis sorry
qed

`There are two things wrong here. First, ?thesis is not a term abbreviation in the
``induction proof, so I get a corresponding error there. Second, the sub-cases are missing.
`
I would have expected an outline like the following:
case Nil
{ case 1
then show ?case sorry
next
case 2
then show ?case sorry
}
next
case (Cons a xs)
{ case 1
then show ?case sorry
next
case 2
then show ?case sorry
}
qed
Are you aware of the problem?
Best,
Andreas

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*