--- a/doc-src/IsarRef/isar-ref.tex Fri Mar 17 22:51:05 2000 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Fri Mar 17 22:51:24 2000 +0100
@@ -33,7 +33,7 @@
\renewcommand{\phi}{\varphi}
-%\includeonly{refcard}
+\includeonly{refcard}
@@ -62,12 +62,12 @@
Any of the Isabelle/Isar commands may be executed in single-steps, so
basically the interpreter has a proof text debugger already built-in.
- Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs
- interface for interactive proof assistants of LFCS Edinburgh, we arrive at a
- reasonable environment for \emph{live document editing}. Thus proof texts
- may be developed incrementally by issuing proper document constructors,
- including forward and backward tracing of partial documents; intermediate
- states may be inspected by diagnostic commands.
+ Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
+ interface for interactive proof assistants, we arrive at a reasonable
+ environment for \emph{live document editing}. Thus proof texts may be
+ developed incrementally by issuing proper document constructors, including
+ forward and backward tracing of partial documents; intermediate states may
+ be inspected by diagnostic commands.
The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
implementation. Theories, theorems, proof procedures etc.\ may be used