--- a/doc-src/IsarRef/isar-ref.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Sat Sep 04 20:57:32 1999 +0200
@@ -67,7 +67,8 @@
implementation. Theories, theorems, proof procedures etc.\ may be used
interchangeably between Isabelle-classic proof scripts and Isabelle/Isar
documents. Isar is as generic as Isabelle, able to support a wide range of
- object-logics. The current end-user setup is mainly for Isabelle/HOL.
+ object-logics. The current working environment for end-users is setup
+ mainly for Isabelle/HOL.
\end{abstract}
\pagenumbering{roman} \tableofcontents \clearfirst
@@ -80,7 +81,6 @@
\nocite{Syme:1997:DECLARE}
\nocite{Syme:1998:thesis}
\nocite{Syme:1999:TPHOL}
-\nocite{Wenzel:1999:TPHOL}
\include{intro}
\include{basics}