Structured Proofs in Isar/HOL

Tobias Nipkow

Isar is an extension of the theorem prover Isabelle with a language for writing human-readable structured proofs. This paper is an introduction to the basic constructs of this language.

pdf ps

BibTeX:

@inproceedings{Nipkow-TYPES02,author={Tobias Nipkow},
title={{Structured Proofs in Isar/HOL}},
booktitle={Types for Proofs and Programs (TYPES 2002)},
editor={H. Geuvers and F. Wiedijk},
year=2003,publisher=Springer,series=LNCS,volume=2646,pages={259-278}}