[isabelle] Converting apply-style induction to Structured Isar
I have a hard time going from Apply-style induction proofs to the
In the apply-style case, the proof of "cata_uniq" is a mere 4 lines:
In the structured style, I need to write much more:
Is there a way to make a concise structured proof of this fact?
This archive was generated by a fusion of
Pipermail (Mailman edition) and