\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!20}{\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: