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


@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},