1+ ===================================================================== + 2| HOL DISTRIBUTION DIRECTORY: Manual/LaTeX | 3+ ===================================================================== + 4 5This directory contains the LaTeX style file and macro definitions for the 6HOL manual. The contents are: 7 8 * READ-ME : This file 9 * ack.tex : Acknowledgements chapter for all three manual volumes 10 * commands.tex : General macro definitions for the manual 11 * layout.sty : File specifying layout style for docs. 12 * layout.tex : Test file for manual page layout 13 * makeindex : The index-making program 14 * pic-macros.tex : Extra macros for picture mode 15 * ref-macros.tex : Reference manual macros for typesetting .doc files 16 17