[isabelle-dev] New tutorial Programming and Proving in Isabelle/HOL

[Tobias Nipkow]

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.