New book: Isabelle/HOL Tutorial
- YOU ALWAYS WANTED TO TRY AN INTERACTIVE THEOREM PROVER,
but they looked so complicated.
- YOU ARE ALREADY USING ONE,
but the documentation ...
LOOK NO FURTHER!
We are pleased to announce the publication of the Isabelle/HOL tutorial
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
by Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel
Springer LNCS 2283
This book is a self-contained introduction to interactive proof in
higher-order logic (HOL), using the proof assistant Isabelle2002. It is a
tutorial for potential users rather than a monograph for researchers.
For more information (and online access!), please visit