[isabelle] Converting apply-style induction to Structured Isar



Hello,

I have a hard time going from Apply-style induction proofs to the
Structured Isar-style.

In the apply-style case, the proof of "cata_uniq" is a mere 4 lines:
http://gawis.dk/misc/apply_sample.thy

In the structured style, I need to write much more:
http://gawis.dk/misc/structured_sample.thy

Is there a way to make a concise structured proof of this fact?

Best regards,
Søren





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