Theorem proving system supporting both interactive proof development and some degree of automation have become quite successful in sizable applications in recent years (e.g. Isabelle/Bali or VerifiCard). Typical examples of this kind of

The *Intelligible semi-automated reasoning* (*Isar*)
approach to readable formal proof documents sets out to bridge the
semantic gap between internal notions of proof given by
state-of-the-art interactive theorem proving systems and an
appropriate level of abstraction for user-level work. The *Isar
formal proof language* has been designed to satisfy quite
contradictory requirements, being both 'declarative' and immediately
'executable', by virtue of the *Isar/VM* interpreter. Compared
to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings:
it is based on a few basic principles only, it is quite independent of
the underlying logic, and integrates a broad range of automated proof
methods. Interactive proof development is supported directly as well.

The Isabelle system offers Isar as an alternative proof language interface layer, beyond traditional tactic scripts. The Isabelle/Isar system provides an interpreter for the Isar formal proof document language. Isabelle/Isar input consists either of proper document constructors, or improper auxiliary commands (for diagnostics, exploration etc.). Proof texts consisting of proper document constructors only admit a purely static reading, thus being intelligible later without requiring dynamic replay that is so typical for traditional proof scripts. Any of the Isabelle/Isar commands may be executed in single-steps, so basically the interpreter has a proof text debugger already built-in.

The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably between Isabelle-classic proof scripts and Isabelle/Isar documents. Isar is as generic as Isabelle, able to support a wide range of object-logics. The current end-user setup is mainly for Isabelle/HOL.

Together with the Isabelle/Isar
instantiation of Proof General, a
generic (X)Emacs interface for interactive proof assistants, we arrive
at a reasonable environment for *live proof document editing*.
Thus proof texts may be developed incrementally by issuing proper
document constructors, including forward and backward tracing of
partial documents; intermediate states may be inspected by diagnostic
commands.

For presentation of the final outcome, Isabelle/Isar provides an
integrated document preparation system based on current PDF/LaTeX
hypertext technology. Thus Isabelle/Isar proof documents may be both
browsed on the WWW, and printed on paper in high quality. E.g. see *Miscellaneous
Isabelle/Isar examples for Higher-Order Logic* or *Lattices
and Orders in Isabelle/HOL*.

Isabelle/Isar also provides a set of emulation commands and proof
methods for embed traditional tactic-style *proof scripts* in a
seamless manner. See *Fundamental
Properties of Lambda-calculus*, for example.

- Gertrud Bauer and Markus Wenzel.
*Computer-Assisted Mathematics at Work - The Hahn-Banach Theorem in Isabelle/Isar*. In T. Coquand, P. Dybjer, B. Nordström, J. Smith, editors,*Types for Proofs and Programs (TYPES'99)*. Lökeberg, Sweden. © Springer LNCS 1956, 2000. - Gertrud Bauer and Markus Wenzel.
*Calculational reasoning revisited - an Isabelle/Isar experience*. In R. J. Boulton and P. B. Jackson, editors,*Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs'2001*, LNCS 2152, © Springer, 2001. - Amine Chaieb and Makarius Wenzel.
*Context aware Calculation and Deduction --- Ring Equalities via Gröbner Bases in Isabelle*. In M. Kauers, M. Kerber, R. Miner, and W. Windsteiger, editors.*Towards Mechanized Mathematical Assistants (CALCULEMUS 2007 and MKM 2007)*. © Springer LNAI 4573, 2007. - Florian Kammüller and Markus Wenzel and Lawrence C. Paulson.
*Locales - A Sectioning Concept for Isabelle*. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors,*Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99*, LNCS 1690, © Springer, 1999. - Tobias Nipkow. Structured
Proofs in Isar/HOL. In
*Types for Proofs and Programs (TYPES 2002)*, LNCS 2646, 2003. - Markus Wenzel.
*Isar - a Generic Interpretative Approach to Readable Formal Proof Documents*. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors,*Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99*, LNCS 1690, © Springer, 1999. Slides available. - Markus Wenzel.
*Isabelle/Isar --- a versatile environment for human-readable formal proof documents*, PhD thesis, Institut für Informatik, Technische Universität München, 2002. Official version (covers Isabelle99-2), unofficial version (covers Isabelle2002). - Markus Wenzel and Free Wiedijk.
*A comparison of the mathematical proof languages Mizar and Isar*. In*Journal of Automated Reasoning***29**, 2002. - Markus Wenzel.
*The Isabelle/Isar Reference Manual*. Part of the Isabelle distribution. TU München, October 2005. - Markus Wenzel.
*Using Axiomatic Type Classes in Isabelle*. Part of the Isabelle distribution. TU München, October 2005. - Markus Wenzel.
*Some aspects of Unix file-system security*. Isabelle/Isar proof document, TU München, October 2005. - Markus Wenzel and Larry Paulson.
*Isabelle/Isar*. In Freek Wiedijk, editor,*The Seventeen Provers of the World*. Springer LNCS 3600, 2006. - Makarius Wenzel.
*Structured Induction Proofs in Isabelle/Isar*. In J. Borwein and W. Farmer, editors,*5th International Conference on Mathematical Knowledge Management, MKM 2006*, LNAI 4108, © Springer, 2006. - Makarius Wenzel.
*Isabelle/Isar --- a generic framework for human-readable proof documents*. In R. Matuszewski and A. Zalewska, editors,*From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec*, Studies in Logic, Grammar, and Rhetoric 10(23), University of Bialystok, 2007.