summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/IsarRef/isar-ref.tex

changeset 7167 | 0b2e3ef1d8f4 |

parent 7135 | 8eabfd7e6b9b |

child 7297 | c1eeeadbe80a |

--- a/doc-src/IsarRef/isar-ref.tex Tue Aug 03 13:16:29 1999 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Tue Aug 03 18:56:51 1999 +0200 @@ -9,8 +9,8 @@ \makeindex -\railterm{lbrace,rbrace,llbrace,rrbrace} -\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim} +\railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace} +\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword} \railalias{name}{\railqtoken{name}} \railalias{nameref}{\railqtoken{nameref}} @@ -37,7 +37,38 @@ \maketitle \begin{abstract} - FIXME + \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic + approach to readable formal proof documents. It sets out to bridge the + semantic gap between any internal notions of proof based on primitive + inferences and tactics, 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 \emph{Isar/VM} interpreter. + + The current version of Isabelle 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 may consist either of \emph{proper document + constructors}, or \emph{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. + + Employing the \emph{ProofGeneral/isar} instantiation of the generic Emacs + interface for interactive proof assistants of LFCS Edinburgh, we arrive at a + reasonable environment for \emph{live 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. + + The Isar subsystem of Isabelle 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. \end{abstract} \pagenumbering{roman} \tableofcontents \clearfirst