\documentclass[11pt,a4paper]{book}
\usepackage[latin1]{inputenc}
\usepackage{amsmath,amsthm}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{charter}
\usepackage[pdftex]{graphicx}
\usepackage{proof}
\usepackage{url}
\usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
\usepackage{lineno}
\usepackage{xcolor}
\usepackage{framed}
\usepackage{boxedminipage}
\usepackage{mathpartir}
\usepackage{flafter}
\usepackage{index}
\usepackage{tocbibind}
\usepackage{tikz}
\usepackage{bashful}
\usetikzlibrary{shadows}
\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}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% indexing
\newindex{default}{idx}{ind}{Index}
\newindex{str}{str}{stu}{Structure Index}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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
\abovecaptionskip 1mm
\belowcaptionskip 10mm
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hyphenation{Isabelle}
\renewcommand{\isasymiota}{}
\renewcommand{\isamarkupsubsection}[1]{\subsection*{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% to work around a problem with \isanewline
\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% for exercises, comments and readmores
\newtheoremstyle{exercisestyle}{\topsep}{\topsep}{\small\it}{}{\small\bfseries}{:}{1ex}{}
\theoremstyle{exercisestyle}
\newtheorem{exercise}{Exercise}[section]
\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}

\newcommand{\readmoremarginpar}[1]%
{\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}

\newenvironment{leftrightbar}{%
\def\FrameCommand##1{\vrule width 2pt \hspace{8pt}##1\hspace{8pt}\vrule width 2pt}%
\MakeFramed {\advance\hsize-\width \FrameRestore}}%
{\endMakeFramed}

\newenvironment{readmore}%
{\begin{leftrightbar}\small\it{\textbf{Read More}}\\}{\end{leftrightbar}}
\newenvironment{conventions}%
{\begin{leftrightbar}\small\it{\textbf{Coding Conventions / Rules of Thumb}}}{\end{leftrightbar}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% some mathematical notation
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% this is to draw a gray box around code
%(FIXME redefine pagebreak so that it includes a \smallskip)
\newenvironment{graybox}
{\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\smallskip\FrameRestore}}
{\smallskip\endMakeFramed}
\newenvironment{grayboxwithoutsep}
{\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\FrameRestore}}
{\endMakeFramed}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% this hack is for getting rid of the ML {* ... *} 
% scaffolding around function definitions
\newenvironment{vanishML}{%
\renewcommand{\isacommand}[1]{}%
\renewcommand{\isacartoucheopen}{}%
\renewcommand{\isacartoucheclose}{}}{}

\isakeeptag{grayML}
\renewcommand{\isataggrayML}{\begin{vanishML}\begin{graybox}}
\renewcommand{\endisataggrayML}{\end{graybox}\end{vanishML}}

\isakeeptag{linenosgrayML}
\renewcommand{\isataglinenosgrayML}{\begin{vanishML}\begin{graybox}\begin{linenos}}
\renewcommand{\endisataglinenosgrayML}{\end{linenos}\end{graybox}\end{vanishML}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% for code that has line numbers
\newenvironment{linenos}{\resetlinenumber\internallinenumbers}{\par\nolinenumbers}

\isakeeptag{linenos}
\renewcommand{\isataglinenos}{\begin{linenos}}
\renewcommand{\endisataglinenos}{\end{linenos}}

% should be used in ML code
\isakeeptag{linenosgray}
\renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}}
\renewcommand{\endisataglinenosgray}{\end{linenos}\end{graybox}\end{vanishML}}

\isakeeptag{graylinenos}
\renewcommand{\isataggraylinenos}{\begin{graybox}\begin{linenos}}
\renewcommand{\endisataggraylinenos}{\end{linenos}\end{graybox}}

\isakeeptag{gray}
\renewcommand{\isataggray}{\begin{graybox}}
\renewcommand{\endisataggray}{\end{graybox}}

\isakeeptag{small}
\renewcommand{\isatagsmall}{\begingroup\small}
\renewcommand{\endisatagsmall}{\endgroup}

% for code that should not be printed
\isakeeptag{no}
\renewcommand{\isatagno}{}
\renewcommand{\endisatagno}{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewenvironment{isabelle}
{\begin{trivlist}\begin{isabellebody}\small\item\relax}
{\end{isabellebody}\end{trivlist}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% for {*  *} in antiquotations
%\newcommand{\isasymverbopen}{\isacharverbatimopen}
%\newcommand{\isasymverbclose}{\isacharverbatimclose}
\newcommand{\isasymverbopen}{\isacartoucheopen}
\newcommand{\isasymverbclose}{\isacartoucheclose}
\newcommand{\isasymfoo}{\isa{{\isacharbackslash}{\isacharless}foo{\isachargreater}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% since * cannot be used in text {*...*} 
\newenvironment{tabularstar}[2]
{\begin{tabular*}{#1}{#2}}{\end{tabular*}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% short hands
\def\simpleinductive{\isacommand{simple\isacharunderscore{}inductive}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}

\title{\mbox{}\\[-10ex]
       \includegraphics[scale=0.5]{tutorial-logo.jpg}\\[3ex]
       {\huge\bf The Isabelle Cookbook}\\
       \mbox{A Gentle Tutorial for Programming Isabelle/ML}\\ (draft)}

\author{by Christian Urban with contributions from:\\[2ex] 
        \begin{tabular}{r@{\hspace{1.8mm}}l}
        Stefan & Berghofer\\
        Jasmin & Blanchette\\
        Sascha & Böhme\\
        Lukas & Bulwahn\\
        Jeremy & Dawson\\
        Rafal & Kolanski\\
        Alexander & Krauss\\
        Tobias & Nipkow\\
        Norbert & Schirmer\\
        Andreas & Schropp\\
        Christian & Sternagel\\ 
        \end{tabular}}

\maketitle

% table of contents
\frontmatter
\setcounter{tocdepth}{1}
\tableofcontents

% generated text of all theories
\mainmatter
\input{session}

% bibliography
\backmatter
\bibliographystyle{abbrv}
\bibliography{root}

% indices
\setindexname{Structure Index}
\printindex[str]
\setindexname{Index}
\printindex

\end{document}

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