\documentclass[11pt,a4paper]{report}
\usepackage[latin1]{inputenc}
\usepackage{amsmath,amsthm}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{charter}
\usepackage[pdftex]{graphicx}
\usepackage{proof}
\usepackage{alltt}
\usepackage{rail}
\usepackage{url}
\usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
\usepackage{lineno}
\usepackage{boxedminipage}
\usepackage{xcolor}
\usepackage{pdfsetup}
\urlstyle{rm}
\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
\renewcommand{\isastyleminor}{\tt\slshape}%
\renewcommand{\isastyle}{\small\tt\slshape}%
\isadroptag{theory}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% For cross references to the 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}]}
\externaldocument[R-]{isar-ref}
\newcommand{\isarref}[1]{\ref{R-#1}}
\newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]}
\newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% sane default for proof documents
\parindent 0pt\parskip 0.6ex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hyphenation{Isabelle}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% to work around a problem with \isanewline
\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% for exercises, comments and readmores
\newtheorem{exercise}{Exercise}[section]
\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
\newcommand{\readmoremarginpar}[1]%
{\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}
\newenvironment{readmore}%
{\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% this is to draw a gray box around code
\makeatletter\newenvironment{graybox}{%
\begin{lrbox}{\@tempboxa}\begin{minipage}{0.985\textwidth}}{\end{minipage}\end{lrbox}%
\colorbox{gray!10}{\usebox{\@tempboxa}}
}\makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% this hack is for getting rid of the ML {* ... *}
% scaffolding around function definitions
\newenvironment{vanishML}{%
\renewcommand{\isacommand}[1]{}%
\renewcommand{\isacharverbatimopen}{}%
\renewcommand{\isacharverbatimclose}{}}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% for code
\isakeeptag{CookBookML}
\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{isabelle}\begin{graybox}}
\renewcommand{\endisatagCookBookML}{\end{graybox}\end{isabelle}\end{vanishML}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% for code that has line numbers
\isakeeptag{linenumbers}
\renewcommand{\isataglinenumbers}
{\begin{vanishML}\begin{isabelle}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
\renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{isabelle}\end{vanishML}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewenvironment{isabelle}
{\begin{trivlist}\begin{isabellebody}\small\item\relax}
{\end{isabellebody}\end{trivlist}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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}{r@{\hspace{1.8mm}}l}
Stefan & Berghofer\\
Sascha & Böhme\\
Jeremy & Dawson\\
Alexander & Krauss\\
\end{tabular}}
\maketitle
\tableofcontents
% generated text of all theories
\input{session}
\newpage
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: