\documentclass[11pt,a4paper]{report}
\usepackage{amsmath,amsthm}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{charter}
\usepackage[pdftex]{graphicx}

% Cross references to other manuals:
\usepackage{xr}
\externaldocument[I-]{implementation}
\newcommand{\impref}[1]{\ref{I-#1}}
\newcommand{\ichcite}[1]{[Impl.\,Man., ch.~\impref{#1}]}
\newcommand{\isccite}[1]{[Impl.\,Man., sec.~\impref{#1}]}

\usepackage{pdfsetup}

\urlstyle{rm}
\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
\renewcommand{\isastyle}{\isastyleminor}% use same formatting for txt and text
\isadroptag{theory}

\newenvironment{readmore}
{\makebox[0pt][r]{\fbox{\textbf{Read More}}~~}\it}{}

\newtheorem{exercise}{Exercise}[section]


\begin{document}

\title{\mbox{}\\[-10ex]
       \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
       The Isabelle Programmer's Cookbook (fragment)}
\author{with contributions by:\\[2ex] 
        \begin{tabular}{l}
        Alexander Krauss\\ 
        Jeremy Dawson\\
        Stefan Berghofer
        \end{tabular}}
\maketitle

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

\newpage
\bibliographystyle{abbrv}
\bibliography{manul,cookbook}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: