remove unnecessary number-representation-specific rules from metis calls;
speed up another proof
\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}