\documentclass[11pt,a4paper]{report}+
−
\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{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}}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
+
−
\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}{l}+
−
        Alexander Krauss\\ +
−
        Jeremy Dawson\\+
−
        Stefan Berghofer+
−
        \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:+
−