1.1 --- a/doc-src/IsarRef/isar-ref.tex	Wed Jan 02 21:52:54 2002 +0100
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Wed Jan 02 21:53:50 2002 +0100
     1.3 @@ -67,42 +67,6 @@
     1.4  
     1.5  \maketitle 
     1.6  
     1.7 -\begin{abstract}
     1.8 -  \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
     1.9 -  approach to readable formal proof documents.  It sets out to bridge the
    1.10 -  semantic gap between any internal notions of proof based on primitive
    1.11 -  inferences and tactics, and an appropriate level of abstraction for
    1.12 -  user-level work.  The Isar formal proof language has been designed to
    1.13 -  satisfy quite contradictory requirements, being both ``declarative'' and
    1.14 -  immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
    1.15 -  
    1.16 -  The Isabelle/Isar system provides an interpreter for the Isar formal proof
    1.17 -  language.  The input may consist either of proper document constructors, or
    1.18 -  improper auxiliary commands (for diagnostics, exploration etc.).  Proof
    1.19 -  texts consisting of proper elements only admit a purely static reading, thus
    1.20 -  being intelligible later without requiring dynamic replay that is so typical
    1.21 -  for traditional proof scripts.  Any of the Isabelle/Isar commands may be
    1.22 -  executed in single-steps, so basically the interpreter has a proof text
    1.23 -  debugger already built-in.
    1.24 -  
    1.25 -  Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
    1.26 -  interface for interactive proof assistants, we arrive at a reasonable
    1.27 -  environment for \emph{live document editing}.  Thus proof texts may be
    1.28 -  developed incrementally by issuing proof commands, including forward and
    1.29 -  backward tracing of partial documents; intermediate states may be inspected
    1.30 -  by diagnostic commands.
    1.31 -  
    1.32 -  The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
    1.33 -  implementation.  Theories, theorems, proof procedures etc.\ may be used
    1.34 -  interchangeably between classic Isabelle proof scripts and Isabelle/Isar
    1.35 -  documents.  Even more, Isar provides a set of emulation commands and methods
    1.36 -  for simulating traditional tactic scripts within new-style theory documents.
    1.37 -  
    1.38 -  The Isar framework is as generic as Isabelle, able to support a wide range
    1.39 -  of object-logics.  Currently, the end-user working environment is most
    1.40 -  complete for Isabelle/HOL.
    1.41 -\end{abstract}
    1.42 -
    1.43  \pagenumbering{roman} \tableofcontents \clearfirst
    1.44  
    1.45  %FIXME
    1.46 @@ -126,6 +90,7 @@
    1.47  \include{pure}
    1.48  \include{generic}
    1.49  \include{hol}
    1.50 +\include{zf}
    1.51  
    1.52  \appendix
    1.53  \include{refcard}