Interactive Proof: Introduction to Isabelle/HOL

Tobias Nipkow

This paper introduces interactive theorem proving with the Isabelle/HOL system. The following topics are covered: We assume basic familiarity with some functional programming language of the ML or Haskell family, in particular with recursive data types and pattern matching. No specific background in logic is necessary beyond the ability to read predicate logic formulas.


@inproceedings{Nipkow-MOD2011,author={Tobias Nipkow},
title={Interactive Proof: Introduction to {Isabelle/HOL}},
booktitle={Software Safety and Security},
publisher={IOS Press},editor={O. Grumberg and T. Nipkow and B. Hauptmann},
This article is superseded by the manual Programming and Proving in Isabelle/HOL.