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
