# HG changeset patch
# User wenzelm
# Date 941379955 -3600
# Node ID feea893b47c7a9b94a7722049c99fdbcf43fb86d
# Parent  d9aef93c0e324029896c2e353f7b35c86ccd5661
tuned;

diff -r d9aef93c0e32 -r feea893b47c7 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Sun Oct 31 15:20:35 1999 +0100
+++ b/doc-src/IsarRef/isar-ref.tex	Sun Oct 31 15:25:55 1999 +0100
@@ -87,6 +87,7 @@
 \nocite{Syme:1997:DECLARE}
 \nocite{Syme:1998:thesis}
 \nocite{Syme:1999:TPHOL}
+\nocite{Zammit:1999:TPHOL}
 
 \include{intro}
 \include{basics}
diff -r d9aef93c0e32 -r feea893b47c7 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sun Oct 31 15:20:35 1999 +0100
+++ b/doc-src/IsarRef/pure.tex	Sun Oct 31 15:25:55 1999 +0100
@@ -804,8 +804,8 @@
   but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
 \end{descr}
 
-A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
-goals and facts are available as well.  For any open goal,
+A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
+and facts are available as well.  For any open goal,
 $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
 (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
 (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its