# HG changeset patch
# User wenzelm
# Date 966271410 -7200
# Node ID a585662e6490cbac228865230fca1a6baca029dd
# Parent  48d438b316c99e667d2396e051ac18299b593f24
some more refs;

diff -r 48d438b316c9 -r a585662e6490 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Mon Aug 14 18:42:57 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Aug 14 18:43:30 2000 +0200
@@ -1,6 +1,13 @@
 
 %% $Id$
 
+% FIXME TODO
+%
+% - update Proof General and X-symbol installation notes;
+% - update tactic emulation (including refcard);
+% - proof script conversion guide;
+
+
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{latexsym,graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
 
@@ -97,17 +104,18 @@
 \pagenumbering{roman} \tableofcontents \clearfirst
 
 %FIXME
-% - HahnBanach paper
-% - Freek Widijk's stuff
-
-%FIXME
+\nocite{Aspinall:2000:eProof}
+\nocite{Bauer-Wenzel:2000:HB}
+\nocite{Harrison:1996:MizarHOL}
+\nocite{Muzalewski:Mizar}
 \nocite{Rudnicki:1992:MizarOverview}
-\nocite{Harrison:1996:MizarHOL}
 \nocite{Rudnicki:1992:MizarOverview}
-\nocite{Trybulec:1993:MizarFeatures}
 \nocite{Syme:1997:DECLARE}
 \nocite{Syme:1998:thesis}
 \nocite{Syme:1999:TPHOL}
+\nocite{Trybulec:1993:MizarFeatures}
+\nocite{Wiedijk:1999:Mizar}
+\nocite{Wiedijk:2000:MV}
 \nocite{Zammit:1999:TPHOL}
 
 \include{intro}
@@ -119,6 +127,7 @@
 
 \appendix
 \include{refcard}
+\include{conversion}
 
 \begingroup
   \bibliographystyle{plain} \small\raggedright\frenchspacing