# HG changeset patch
# User wenzelm
# Date 953329884 -3600
# Node ID daec9cef376dfbfe8d9a01bba5ef6951c4848383
# Parent  76d8d8aab881fe7a8de4416b2e3bc7eec156ccda
tuned;

diff -r 76d8d8aab881 -r daec9cef376d doc-src/IsarRef/isar-ref.tex
--- 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