ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
\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}