\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}\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{\isacharverbatimopen}{}%\renewcommand{\isacharverbatimclose}{}}{}\isakeeptag{TutorialML}\renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}}\renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}}\isakeeptag{TutorialMLprf}\renewcommand{\isatagTutorialMLprf}{\begin{grayboxwithoutsep}}\renewcommand{\endisatagTutorialMLprf}{\end{grayboxwithoutsep}}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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{\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 on the ML-Level of Isabelle}\\ (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\\ Alexander & Krauss\\ Tobias & Nipkow\\ 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: