4 \usepackage{isabelle} |
4 \usepackage{isabelle} |
5 \usepackage{isabellesym} |
5 \usepackage{isabellesym} |
6 \usepackage{charter} |
6 \usepackage{charter} |
7 \usepackage[pdftex]{graphicx} |
7 \usepackage[pdftex]{graphicx} |
8 \usepackage{proof} |
8 \usepackage{proof} |
9 \usepackage{alltt} |
|
10 \usepackage{rail} |
9 \usepackage{rail} |
11 \usepackage{url} |
10 \usepackage{url} |
12 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry} |
11 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry} |
13 \usepackage{lineno} |
12 \usepackage{lineno} |
14 \usepackage{boxedminipage} |
|
15 \usepackage{xcolor} |
13 \usepackage{xcolor} |
|
14 \usepackage{framed} |
16 \usepackage{pdfsetup} |
15 \usepackage{pdfsetup} |
17 |
16 |
18 \urlstyle{rm} |
17 \urlstyle{rm} |
19 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text |
18 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text |
20 \renewcommand{\isastyleminor}{\tt\slshape}% |
19 \renewcommand{\isastyleminor}{\tt\slshape}% |
33 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} |
32 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} |
34 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} |
33 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} |
35 |
34 |
36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
37 % sane default for proof documents |
36 % sane default for proof documents |
38 \parindent 0pt\parskip 0.6ex |
37 \parindent 0pt |
39 |
38 \parskip 0.6ex |
|
39 \abovecaptionskip -3mm |
|
40 \belowcaptionskip 10mm |
40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
41 \hyphenation{Isabelle} |
42 \hyphenation{Isabelle} |
42 |
43 |
43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
44 % to work around a problem with \isanewline |
45 % to work around a problem with \isanewline |
53 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} |
54 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} |
54 |
55 |
55 \newenvironment{readmore}% |
56 \newenvironment{readmore}% |
56 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} |
57 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} |
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 %(FIXME redefine pagebreak so that it includes a \smallskip) |
62 \begin{lrbox}{\@tempboxa}\begin{minipage}{0.985\textwidth}}{\end{minipage}\end{lrbox}% |
62 \newenvironment{graybox} |
63 \colorbox{gray!20}{\usebox{\@tempboxa}} |
63 {\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\smallskip\FrameRestore}} |
64 }\makeatother |
64 {\smallskip\endMakeFramed} |
65 |
65 |
66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
67 % this hack is for getting rid of the ML {* ... *} |
67 % this hack is for getting rid of the ML {* ... *} |
68 % scaffolding around function definitions |
68 % scaffolding around function definitions |
69 \newenvironment{vanishML}{% |
69 \newenvironment{vanishML}{% |
70 \renewcommand{\isacommand}[1]{}% |
70 \renewcommand{\isacommand}[1]{}% |
71 \renewcommand{\isacharverbatimopen}{}% |
71 \renewcommand{\isacharverbatimopen}{}% |
72 \renewcommand{\isacharverbatimclose}{}}{} |
72 \renewcommand{\isacharverbatimclose}{}}{} |
73 |
73 |
74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
75 % for code |
|
76 \isakeeptag{CookBookML} |
74 \isakeeptag{CookBookML} |
77 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{isabelle}\begin{graybox}} |
75 \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}} |
78 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{isabelle}\end{vanishML}} |
76 \renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}} |
79 |
77 |
80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
81 % for code that has line numbers |
79 % for code that has line numbers |
82 \isakeeptag{linenumbers} |
80 \isakeeptag{linenumbers} |
83 \renewcommand{\isataglinenumbers} |
81 \renewcommand{\isataglinenumbers}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers} |
84 {\begin{vanishML}\begin{isabelle}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers} |
82 \renewcommand{\endisataglinenumbers}{\par\end{graybox}\end{vanishML}} |
85 \renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{isabelle}\end{vanishML}} |
|
86 |
83 |
87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
88 \renewenvironment{isabelle} |
85 \renewenvironment{isabelle} |
89 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
86 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
90 {\end{isabellebody}\end{trivlist}} |
87 {\end{isabellebody}\end{trivlist}} |