avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube);
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{amssymb}
\usepackage[greek,english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{textcomp}
\usepackage{latexsym}
\usepackage{graphicx}
\let\intorig=\int %iman.sty redefines \int
\usepackage{../iman,../extra,../isar,../proof}
\usepackage[nohyphen,strings]{../underscore}
\usepackage{../../lib/texinputs/isabelle}
\usepackage{../../lib/texinputs/isabellesym}
\usepackage{../../lib/texinputs/railsetup}
\usepackage{../ttbox}
\usepackage{supertabular}
\usepackage{style}
\usepackage{../pdfsetup}
\hyphenation{Isabelle}
\hyphenation{Isar}
\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
\author{\emph{Makarius Wenzel} \\[3ex]
With Contributions by
Clemens Ballarin,
Stefan Berghofer, \\
Jasmin Blanchette,
Timothy Bourke,
Lukas Bulwahn, \\
Lucas Dixon,
Florian Haftmann,
Gerwin Klein, \\
Alexander Krauss,
Tobias Nipkow,
Lars Noschinski, \\
David von Oheimb,
Larry Paulson,
Sebastian Skalberg
}
\makeindex
\chardef\charbackquote=`\`
\newcommand{\backquote}{\mbox{\tt\charbackquote}}
\begin{document}
\maketitle
\pagenumbering{roman}
{\def\isamarkupchapter#1{\chapter*{#1}}\input{Thy/document/Preface.tex}}
\tableofcontents
\clearfirst
\part{Basic Concepts}
\input{Thy/document/Synopsis.tex}
\input{Thy/document/Framework.tex}
\input{Thy/document/First_Order_Logic.tex}
\part{General Language Elements}
\input{Thy/document/Outer_Syntax.tex}
\input{Thy/document/Document_Preparation.tex}
\input{Thy/document/Spec.tex}
\input{Thy/document/Proof.tex}
\input{Thy/document/Inner_Syntax.tex}
\input{Thy/document/Misc.tex}
\input{Thy/document/Generic.tex}
\part{Object-Logics}
\input{Thy/document/HOL_Specific.tex}
\input{Thy/document/HOLCF_Specific.tex}
\input{Thy/document/ZF_Specific.tex}
\part{Appendix}
\appendix
\input{Thy/document/Quick_Reference.tex}
\let\int\intorig
\input{Thy/document/Symbols.tex}
\input{Thy/document/ML_Tactic.tex}
\begingroup
\bibliographystyle{abbrv} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup
\printindex
\end{document}