--- a/doc-src/HOL/logics-HOL.tex Mon Sep 26 19:19:15 2005 +0200
+++ b/doc-src/HOL/logics-HOL.tex Mon Sep 26 20:12:51 2005 +0200
@@ -1,6 +1,6 @@
%% $Id$
\documentclass[12pt,a4paper]{report}
-\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
+\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,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}
@@ -28,6 +28,8 @@
\hrule\bigskip}
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
+\newcommand\bs{\char '134 } % A backslash character for \tt font
+
\makeindex
\underscoreoff