1.1 --- a/doc-src/IsarRef/isar-ref.tex	Tue Mar 21 15:32:08 2000 +0100
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Tue Mar 21 17:32:43 2000 +0100
     1.3 @@ -53,20 +53,20 @@
     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 proper
     1.8 -  document constructors, or improper auxiliary commands (for diagnostics,
     1.9 -  exploration etc.).  Proof texts consisting of proper document constructors
    1.10 -  only, admit a purely static reading, thus being intelligible later without
    1.11 -  requiring dynamic replay that is so typical for traditional proof scripts.
    1.12 -  Any of the Isabelle/Isar commands may be executed in single-steps, so
    1.13 -  basically the interpreter has a proof text debugger already built-in.
    1.14 +  Isar formal proof language.  The input may consist either of proper document
    1.15 +  constructors, or improper auxiliary commands (for diagnostics, exploration
    1.16 +  etc.).  Proof texts consisting of proper elements only, admit a purely
    1.17 +  static reading, thus being intelligible later without requiring dynamic
    1.18 +  replay that is so typical for traditional proof scripts.  Any of the
    1.19 +  Isabelle/Isar commands may be executed in single-steps, so basically the
    1.20 +  interpreter has a proof text debugger already built-in.
    1.21    
    1.22    Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
    1.23    interface for interactive proof assistants, we arrive at a reasonable
    1.24    environment for \emph{live document editing}.  Thus proof texts may be
    1.25 -  developed incrementally by issuing proper document constructors, including
    1.26 -  forward and backward tracing of partial documents; intermediate states may
    1.27 -  be inspected by diagnostic commands.
    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