7 \usepackage{proof} |
7 \usepackage{proof} |
8 \usepackage{alltt} |
8 \usepackage{alltt} |
9 \usepackage{rail} |
9 \usepackage{rail} |
10 \usepackage{url} |
10 \usepackage{url} |
11 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry} |
11 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry} |
|
12 \usepackage{pdfsetup} |
12 |
13 |
13 % Cross references to other manuals: |
14 \urlstyle{rm} |
|
15 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text |
|
16 \renewcommand{\isastyleminor}{\tt\slshape}% |
|
17 \renewcommand{\isastyle}{\small\tt\slshape}% |
|
18 \isadroptag{theory} |
|
19 |
|
20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
21 % For cross references to the other manuals: |
14 \usepackage{xr} |
22 \usepackage{xr} |
15 \externaldocument[I-]{implementation} |
23 \externaldocument[I-]{implementation} |
16 \newcommand{\impref}[1]{\ref{I-#1}} |
24 \newcommand{\impref}[1]{\ref{I-#1}} |
17 \newcommand{\ichcite}[1]{[Impl.\,Man., Ch.~\impref{#1}]} |
25 \newcommand{\ichcite}[1]{[Impl.\,Man., Ch.~\impref{#1}]} |
18 \newcommand{\isccite}[1]{[Impl.\,Man., Sec.~\impref{#1}]} |
26 \newcommand{\isccite}[1]{[Impl.\,Man., Sec.~\impref{#1}]} |
19 \externaldocument[R-]{isar-ref} |
27 \externaldocument[R-]{isar-ref} |
20 \newcommand{\isarref}[1]{\ref{R-#1}} |
28 \newcommand{\isarref}[1]{\ref{R-#1}} |
21 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} |
29 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} |
22 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} |
30 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} |
23 |
31 |
24 \usepackage{pdfsetup} |
32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
25 |
|
26 \urlstyle{rm} |
|
27 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text |
|
28 \renewcommand{\isastyleminor}{\tt\slshape}% |
|
29 \renewcommand{\isastyle}{\small\tt\slshape}% |
|
30 \isadroptag{theory} |
|
31 |
|
32 % sane default for proof documents |
33 % sane default for proof documents |
33 \parindent 0pt\parskip 0.6ex |
34 \parindent 0pt\parskip 0.6ex |
34 |
35 |
35 % for comments on the margin |
36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
37 % to work around a problem with \isanewline |
|
38 \renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}} |
|
39 |
|
40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
41 % FIXME: WHAT DOES THIS DO? |
|
42 \renewenvironment{isabelle} |
|
43 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
|
44 {\end{isabellebody}\end{trivlist}} |
|
45 |
|
46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
47 % for exercises, comments and readmores |
|
48 \newtheorem{exercise}{Exercise}[section] |
|
49 \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} |
|
50 |
36 \newcommand{\readmoremarginpar}[1]% |
51 \newcommand{\readmoremarginpar}[1]% |
37 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} |
52 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} |
38 |
53 |
39 \newenvironment{readmore}% |
54 \newenvironment{readmore}% |
40 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} |
55 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} |
41 |
56 |
42 % to work around a problem with \isanewline |
57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
43 \renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}} |
58 % FIXME: THIS SHOULD NOT BE USED ANYMORE |
44 |
|
45 \renewenvironment{isabelle} |
|
46 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
|
47 {\end{isabellebody}\end{trivlist}} |
|
48 |
|
49 % for exercises and comments |
|
50 \newtheorem{exercise}{Exercise}[section] |
|
51 \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} |
|
52 |
|
53 % a table environment with proper indentation |
59 % a table environment with proper indentation |
54 \newenvironment{mytable}{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}{\end{tabular}\end{trivlist}} |
60 \newenvironment{mytable} |
|
61 {\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}} |
|
62 {\end{tabular}\end{trivlist}} |
55 |
63 |
56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
57 \hyphenation{Isabelle} |
65 \hyphenation{Isabelle} |
|
66 |
|
67 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
68 % this hack is for getting rid of the ML {* ... *} |
|
69 % scaffolding around function definitions |
|
70 \newenvironment{vanishML}{% |
|
71 \renewcommand{\isacommand}[1]{}% |
|
72 \renewcommand{\isacharverbatimopen}{}% |
|
73 \renewcommand{\isacharverbatimclose}{}% |
|
74 \hspace{-1.5mm}\mbox{}}{} |
|
75 |
|
76 \renewcommand{\isatagML}{\begin{vanishML}} |
|
77 \renewcommand{\endisatagML}{\end{vanishML}} |
|
78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
58 |
79 |
59 \begin{document} |
80 \begin{document} |
60 |
81 |
61 \title{\mbox{}\\[-10ex] |
82 \title{\mbox{}\\[-10ex] |
62 \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] |
83 \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] |