1.1 --- a/doc-src/IsarRef/isar-ref.tex	Sat Oct 30 20:12:23 1999 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Sat Oct 30 20:13:16 1999 +0200
     1.3 @@ -54,14 +54,13 @@
     1.4    
     1.5    The current version of Isabelle offers Isar as an alternative proof language
     1.6    interface layer.  The Isabelle/Isar system provides an interpreter for the
     1.7 -  Isar formal proof document language.  The input may consist either of
     1.8 -  \emph{proper document constructors}, or \emph{improper auxiliary commands}
     1.9 -  (for diagnostics, exploration etc.).  Proof texts consisting of proper
    1.10 -  document constructors only, admit a purely static reading, thus being
    1.11 -  intelligible later without requiring dynamic replay that is so typical for
    1.12 -  traditional proof scripts.  Any of the Isabelle/Isar commands may be
    1.13 -  executed in single-steps, so basically the interpreter has a proof text
    1.14 -  debugger already built-in.
    1.15 +  Isar formal proof document language.  The input may consist either of proper
    1.16 +  document constructors, or improper auxiliary commands (for diagnostics,
    1.17 +  exploration etc.).  Proof texts consisting of proper document constructors
    1.18 +  only, admit a purely static reading, thus being intelligible later without
    1.19 +  requiring dynamic replay that is so typical for traditional proof scripts.
    1.20 +  Any of the Isabelle/Isar commands may be executed in single-steps, so
    1.21 +  basically the interpreter has a proof text debugger already built-in.
    1.22    
    1.23    Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs
    1.24    interface for interactive proof assistants of LFCS Edinburgh, we arrive at a