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.7ex |
38 \parindent 0pt\parskip 0.6ex |
39 |
39 |
40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
41 \hyphenation{Isabelle} |
41 \hyphenation{Isabelle} |
42 |
42 |
43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
57 |
57 |
58 |
58 |
59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
60 % this is to draw a gray box around code |
60 % this is to draw a gray box around code |
61 \makeatletter\newenvironment{graybox}{% |
61 \makeatletter\newenvironment{graybox}{% |
62 \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}% |
62 \begin{lrbox}{\@tempboxa}\begin{minipage}{0.985\textwidth}}{\end{minipage}\end{lrbox}% |
63 \colorbox{gray!10}{\usebox{\@tempboxa}} |
63 \colorbox{gray!10}{\usebox{\@tempboxa}} |
64 }\makeatother |
64 }\makeatother |
65 |
65 |
66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
67 % this hack is for getting rid of the ML {* ... *} |
67 % this hack is for getting rid of the ML {* ... *} |
70 \renewcommand{\isacommand}[1]{}% |
70 \renewcommand{\isacommand}[1]{}% |
71 \renewcommand{\isacharverbatimopen}{}% |
71 \renewcommand{\isacharverbatimopen}{}% |
72 \renewcommand{\isacharverbatimclose}{}}{} |
72 \renewcommand{\isacharverbatimclose}{}}{} |
73 |
73 |
74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
75 % for code |
75 \isakeeptag{CookBookML} |
76 \isakeeptag{CookBookML} |
76 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}} |
77 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{isabelle}\begin{graybox}} |
77 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip} |
78 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{isabelle}\end{vanishML}} |
78 |
79 |
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
80 % for line numbers |
81 % for code that has line numbers |
81 \isakeeptag{linenumbers} |
82 \isakeeptag{linenumbers} |
82 \renewcommand{\isataglinenumbers} |
83 \renewcommand{\isataglinenumbers} |
83 {\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers} |
84 {\begin{vanishML}\begin{isabelle}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers} |
84 \renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip} |
85 \renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{isabelle}\end{vanishML}} |
85 |
86 |
86 |
87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
87 |
88 \renewenvironment{isabelle} |
|
89 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
|
90 {\end{isabellebody}\end{trivlist}} |
88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
89 \begin{document} |
92 \begin{document} |
90 |
93 |
91 \title{\mbox{}\\[-10ex] |
94 \title{\mbox{}\\[-10ex] |
92 \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] |
95 \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] |