31 \externaldocument[R-]{isar-ref} |
31 \externaldocument[R-]{isar-ref} |
32 \newcommand{\isarref}[1]{\ref{R-#1}} |
32 \newcommand{\isarref}[1]{\ref{R-#1}} |
33 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} |
33 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} |
34 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} |
34 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} |
35 |
35 |
36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
37 % sane default for proof documents |
37 % sane default for proof documents |
38 \parindent 0pt\parskip 0.6ex |
38 \parindent 0pt\parskip 0.7ex |
39 |
39 |
40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
41 \hyphenation{Isabelle} |
|
42 |
|
43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
41 % to work around a problem with \isanewline |
44 % to work around a problem with \isanewline |
42 \renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}} |
45 \renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}} |
43 |
46 |
44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
45 % FIXME: WHAT DOES THIS DO? |
|
46 \renewenvironment{isabelle} |
|
47 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
|
48 {\end{isabellebody}\end{trivlist}} |
|
49 |
|
50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
51 % for exercises, comments and readmores |
48 % for exercises, comments and readmores |
52 \newtheorem{exercise}{Exercise}[section] |
49 \newtheorem{exercise}{Exercise}[section] |
53 \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} |
50 \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} |
54 |
51 |
55 \newcommand{\readmoremarginpar}[1]% |
52 \newcommand{\readmoremarginpar}[1]% |
56 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} |
53 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} |
57 |
54 |
58 \newenvironment{readmore}% |
55 \newenvironment{readmore}% |
59 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} |
56 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} |
60 |
57 |
61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
62 % FIXME: THIS SHOULD NOT BE USED ANYMORE |
|
63 % a table environment with proper indentation |
|
64 \newenvironment{mytable} |
|
65 {\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}} |
|
66 {\end{tabular}\end{trivlist}} |
|
67 |
58 |
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
69 \hyphenation{Isabelle} |
60 % this is to draw a gray box around code |
|
61 \makeatletter\newenvironment{graybox}{% |
|
62 \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}% |
|
63 \colorbox{gray!10}{\usebox{\@tempboxa}} |
|
64 }\makeatother |
70 |
65 |
71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
72 % this hack is for getting rid of the ML {* ... *} |
67 % this hack is for getting rid of the ML {* ... *} |
73 % scaffolding around function definitions |
68 % scaffolding around function definitions |
74 \newenvironment{vanishML}{% |
69 \newenvironment{vanishML}{% |
75 \renewcommand{\isacommand}[1]{}% |
70 \renewcommand{\isacommand}[1]{}% |
76 \renewcommand{\isacharverbatimopen}{}% |
71 \renewcommand{\isacharverbatimopen}{}% |
77 \renewcommand{\isacharverbatimclose}{}}{} |
72 \renewcommand{\isacharverbatimclose}{}}{} |
78 |
73 |
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
80 \makeatletter\newenvironment{graybox}{% |
|
81 \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}% |
|
82 \colorbox{gray!5}{\usebox{\@tempboxa}} |
|
83 }\makeatother |
|
84 |
|
85 |
|
86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
87 \isakeeptag{CookBookML} |
75 \isakeeptag{CookBookML} |
88 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}} |
76 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}} |
89 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip} |
77 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip} |
90 |
78 |
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
92 % for line numbers |
80 % for line numbers |
93 \isakeeptag{linenumbers} |
81 \isakeeptag{linenumbers} |
94 \renewcommand{\isataglinenumbers} |
82 \renewcommand{\isataglinenumbers} |
95 {\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers} |
83 {\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers} |
96 \renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip} |
84 \renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip} |
97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
98 |
85 |
|
86 |
|
87 |
|
88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
99 \begin{document} |
89 \begin{document} |
100 |
90 |
101 \title{\mbox{}\\[-10ex] |
91 \title{\mbox{}\\[-10ex] |
102 \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] |
92 \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] |
103 The Isabelle Programmer's Cookbook (fragment)} |
93 The Isabelle Programmer's Cookbook (fragment)} |
|
94 |
104 \author{with contributions by:\\[2ex] |
95 \author{with contributions by:\\[2ex] |
105 \begin{tabular}{r@{\hspace{1.8mm}}l} |
96 \begin{tabular}{r@{\hspace{1.8mm}}l} |
106 Stefan & Berghofer\\ |
97 Stefan & Berghofer\\ |
107 Sascha & Böhme\\ |
98 Sascha & Böhme\\ |
108 Jeremy & Dawson\\ |
99 Jeremy & Dawson\\ |
109 Alexander & Krauss\\ |
100 Alexander & Krauss\\ |
110 \end{tabular}} |
101 \end{tabular}} |
|
102 |
111 \maketitle |
103 \maketitle |
112 |
|
113 \tableofcontents |
104 \tableofcontents |
114 |
105 |
115 % generated text of all theories |
106 % generated text of all theories |
116 \input{session} |
107 \input{session} |
117 |
108 |