Getting Started with Isabelle

Jørgen Villadsen

Isabelle is a generic proof assistant available here:


A short "Getting Started with Isabelle" guide: Isabelle.pdf

Sample Isabelle source file used in the guide: Scratch.thy


The full-size screenshot: Isabelle.png

The LaTeX document: Isabelle.tex


The guide is based on a paper by Christian Sternagel available here:



Jørgen Villadsen 2015-02-15