1.1 --- a/doc-src/IsarRef/isar-ref.tex	Sun Oct 31 15:20:35 1999 +0100
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Sun Oct 31 15:25:55 1999 +0100
     1.3 @@ -87,6 +87,7 @@
     1.4  \nocite{Syme:1997:DECLARE}
     1.5  \nocite{Syme:1998:thesis}
     1.6  \nocite{Syme:1999:TPHOL}
     1.7 +\nocite{Zammit:1999:TPHOL}
     1.8  
     1.9  \include{intro}
    1.10  \include{basics}

     2.1 --- a/doc-src/IsarRef/pure.tex	Sun Oct 31 15:20:35 1999 +0100
     2.2 +++ b/doc-src/IsarRef/pure.tex	Sun Oct 31 15:25:55 1999 +0100
     2.3 @@ -804,8 +804,8 @@
     2.4    but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
     2.5  \end{descr}
     2.6  
     2.7 -A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
     2.8 -goals and facts are available as well.  For any open goal,
     2.9 +A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
    2.10 +and facts are available as well.  For any open goal,
    2.11  $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
    2.12  (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
    2.13  (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its