1.1 --- a/doc-src/IsarRef/isar-ref.tex	Mon Aug 14 18:42:57 2000 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Mon Aug 14 18:43:30 2000 +0200
     1.3 @@ -1,6 +1,13 @@
     1.4  
     1.5  %% $Id$
     1.6  
     1.7 +% FIXME TODO
     1.8 +%
     1.9 +% - update Proof General and X-symbol installation notes;
    1.10 +% - update tactic emulation (including refcard);
    1.11 +% - proof script conversion guide;
    1.12 +
    1.13 +
    1.14  \documentclass[12pt,a4paper,fleqn]{report}
    1.15  \usepackage{latexsym,graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
    1.16  
    1.17 @@ -97,17 +104,18 @@
    1.18  \pagenumbering{roman} \tableofcontents \clearfirst
    1.19  
    1.20  %FIXME
    1.21 -% - HahnBanach paper
    1.22 -% - Freek Widijk's stuff
    1.23 -
    1.24 -%FIXME
    1.25 +\nocite{Aspinall:2000:eProof}
    1.26 +\nocite{Bauer-Wenzel:2000:HB}
    1.27 +\nocite{Harrison:1996:MizarHOL}
    1.28 +\nocite{Muzalewski:Mizar}
    1.29  \nocite{Rudnicki:1992:MizarOverview}
    1.30 -\nocite{Harrison:1996:MizarHOL}
    1.31  \nocite{Rudnicki:1992:MizarOverview}
    1.32 -\nocite{Trybulec:1993:MizarFeatures}
    1.33  \nocite{Syme:1997:DECLARE}
    1.34  \nocite{Syme:1998:thesis}
    1.35  \nocite{Syme:1999:TPHOL}
    1.36 +\nocite{Trybulec:1993:MizarFeatures}
    1.37 +\nocite{Wiedijk:1999:Mizar}
    1.38 +\nocite{Wiedijk:2000:MV}
    1.39  \nocite{Zammit:1999:TPHOL}
    1.40  
    1.41  \include{intro}
    1.42 @@ -119,6 +127,7 @@
    1.43  
    1.44  \appendix
    1.45  \include{refcard}
    1.46 +\include{conversion}
    1.47  
    1.48  \begingroup
    1.49    \bibliographystyle{plain} \small\raggedright\frenchspacing