Re: [isabelle] On Recursion Induction



Am 09/05/2012 09:54, schrieb Lars Noschinski:
> This tutorial is a bit dated (but still very useful). I think Tobias Nipkow is
> working on a newer version.

Not a newer version but a completely new and much more compact document
"Programming and Proving in Isabelle/HOL" which you can find for example at
http://isabelle.in.tum.de/website-Isabelle2012-RC2/documentation.html and in the
release in a few weeks. It minimizes "apply" and does not introduce *rule_tac
but structured proofs.

But, as Lars wrote, that tutorial is still useful, but I do not recommend it for
beginners anymore.

Tobias





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