doc-src/HOL/logics-HOL.tex
changeset 7457 e67eed4cd224
parent 6626 a92d2b6e0626
child 7835 e9cd3f3be589
--- a/doc-src/HOL/logics-HOL.tex	Fri Sep 03 16:10:39 1999 +0200
+++ b/doc-src/HOL/logics-HOL.tex	Fri Sep 03 16:11:03 1999 +0200
@@ -1,13 +1,6 @@
 %% $Id$
 \documentclass[12pt]{report}
-\usepackage{graphicx,a4,latexsym,../pdfsetup}
-
-\makeatletter
-\input{../proof.sty}
-\input{../rail.sty}
-\input{../iman.sty}
-\input{../extra.sty}
-\makeatother
+\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
 
 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
 %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}