# HG changeset patch
# User wenzelm
# Date 939747585 -7200
# Node ID e9cd3f3be589b7381880eeb3d4f3ae964b29af2f
# Parent  915be5b9dc6f995c252b4874b41cf7db179e74b0
a4paper;

diff -r 915be5b9dc6f -r e9cd3f3be589 doc-src/HOL/logics-HOL.tex
--- a/doc-src/HOL/logics-HOL.tex	Tue Oct 12 10:24:05 1999 +0200
+++ b/doc-src/HOL/logics-HOL.tex	Tue Oct 12 18:59:45 1999 +0200
@@ -1,6 +1,6 @@
 %% $Id$
-\documentclass[12pt]{report}
-\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
+\documentclass[12pt,a4paper]{report}
+\usepackage{graphicx,../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}