
Isabelle/HOL
A Proof Assistant for HigherOrder Logic
This book is a selfcontained introduction to interactive proof in
higherorder logic (HOL), using the proof assistant
Isabelle2002.
It is a tutorial for
potential users rather than a monograph for researchers.
