# 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