1.1 --- a/doc-src/IsarRef/isar-ref.tex	Fri Mar 17 22:51:05 2000 +0100
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Fri Mar 17 22:51:24 2000 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  \renewcommand{\phi}{\varphi}
     1.6  
     1.7 -%\includeonly{refcard}
     1.8 +\includeonly{refcard}
     1.9  
    1.10  
    1.11  
    1.12 @@ -62,12 +62,12 @@
    1.13    Any of the Isabelle/Isar commands may be executed in single-steps, so
    1.14    basically the interpreter has a proof text debugger already built-in.
    1.15    
    1.16 -  Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs
    1.17 -  interface for interactive proof assistants of LFCS Edinburgh, we arrive at a
    1.18 -  reasonable environment for \emph{live document editing}.  Thus proof texts
    1.19 -  may be developed incrementally by issuing proper document constructors,
    1.20 -  including forward and backward tracing of partial documents; intermediate
    1.21 -  states may be inspected by diagnostic commands.
    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    
    1.29    The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
    1.30    implementation.  Theories, theorems, proof procedures etc.\ may be used