\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{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+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
% to work around a problem with \isanewline+ −
\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
% FIXME: WHAT DOES THIS DO?+ −
\renewenvironment{isabelle}+ −
{\begin{trivlist}\begin{isabellebody}\small\item\relax}+ −
{\end{isabellebody}\end{trivlist}}+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
% 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}{}+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
% FIXME: THIS SHOULD NOT BE USED ANYMORE+ −
% a table environment with proper indentation+ −
\newenvironment{mytable}+ −
{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}+ −
{\end{tabular}\end{trivlist}}+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\hyphenation{Isabelle}+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
% this hack is for getting rid of the ML {* ... *} + −
% scaffolding around function definitions+ −
\newenvironment{vanishML}{%+ −
\renewcommand{\isacommand}[1]{}%+ −
\renewcommand{\isacharverbatimopen}{}%+ −
\renewcommand{\isacharverbatimclose}{}%+ −
\hspace{-1.5mm}\mbox{}}{}+ −
+ −
\renewcommand{\isatagML}{\begin{vanishML}}+ −
\renewcommand{\endisatagML}{\end{vanishML}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
% for line numbers+ −
\isakeeptag{linenumbers}+ −
\renewcommand{\isataglinenumbers}{\begin{vanishML}\begingroup\resetlinenumber\linenumbers}+ −
\renewcommand{\endisataglinenumbers}{\endgroup\end{vanishML}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
\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:+ −