\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:+ −