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