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
This archive was generated by a fusion of
Pipermail (Mailman edition) and