[isabelle-dev] New tutorial Programming and Proving in Isabelle/HOL
nipkow at in.tum.de
Wed Apr 4 10:04:45 CEST 2012
An updated announcement of a new tutorial in the development version of
Isabelle. Comments welcome! [If it does not build on your own machine, your tex
distribution probably lacks the eulervm package.]
* New tutorial "Programming and Proving in Isabelle/HOL".
It completely supercedes "A Tutorial Introduction to Structured Isar Proofs",
which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant
for Higher-Order Logic" as the recommended beginners tutorial
but does not cover all of the material of that old tutorial.
More information about the isabelle-dev