Getting Started with Isabelle

Jørgen Villadsen

Isabelle is a generic proof assistant available here: http://isabelle.in.tum.de/

 

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: http://arxiv.org/abs/1208.1368

 

       Isabelle


Jørgen Villadsen 2015-02-15 http://people.compute.dtu.dk/jovi/Isabelle/