1 \documentclass[11pt,a4paper]{report} |
|
2 \usepackage[latin1]{inputenc} |
|
3 \usepackage{amsmath,amsthm} |
|
4 \usepackage{isabelle} |
|
5 \usepackage{isabellesym} |
|
6 \usepackage{charter} |
|
7 \usepackage[pdftex]{graphicx} |
|
8 \usepackage{proof} |
|
9 \usepackage{rail} |
|
10 \usepackage{url} |
|
11 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry} |
|
12 \usepackage{lineno} |
|
13 \usepackage{xcolor} |
|
14 \usepackage{framed} |
|
15 \usepackage{boxedminipage} |
|
16 \usepackage{mathpartir} |
|
17 \usepackage{pdfsetup} |
|
18 |
|
19 \urlstyle{rm} |
|
20 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text |
|
21 \renewcommand{\isastyleminor}{\tt\slshape}% |
|
22 \renewcommand{\isastyle}{\small\tt\slshape}% |
|
23 \isadroptag{theory} |
|
24 |
|
25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
26 % For cross references to the other manuals: |
|
27 \usepackage{xr} |
|
28 \externaldocument[I-]{implementation} |
|
29 \newcommand{\impref}[1]{\ref{I-#1}} |
|
30 \newcommand{\ichcite}[1]{[Impl.\,Man., Ch.~\impref{#1}]} |
|
31 \newcommand{\isccite}[1]{[Impl.\,Man., Sec.~\impref{#1}]} |
|
32 \externaldocument[R-]{isar-ref} |
|
33 \newcommand{\isarref}[1]{\ref{R-#1}} |
|
34 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} |
|
35 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} |
|
36 |
|
37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
38 % sane default for proof documents |
|
39 \parindent 0pt |
|
40 \parskip 0.6ex |
|
41 \abovecaptionskip 1mm |
|
42 \belowcaptionskip 10mm |
|
43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
44 \hyphenation{Isabelle} |
|
45 \renewcommand{\isasymiota}{} |
|
46 |
|
47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
48 % to work around a problem with \isanewline |
|
49 \renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}} |
|
50 |
|
51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
52 % for exercises, comments and readmores |
|
53 \newtheorem{exercise}{Exercise}[section] |
|
54 \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} |
|
55 |
|
56 \newcommand{\readmoremarginpar}[1]% |
|
57 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} |
|
58 |
|
59 \newenvironment{leftrightbar}{% |
|
60 \def\FrameCommand##1{\vrule width 2pt \hspace{8pt}##1\hspace{8pt}\vrule width 2pt}% |
|
61 \MakeFramed {\advance\hsize-\width \FrameRestore}}% |
|
62 {\endMakeFramed} |
|
63 |
|
64 |
|
65 \newenvironment{readmore}% |
|
66 {\begin{leftrightbar}\small\it{\textbf{Read More}}\\}{\end{leftrightbar}} |
|
67 |
|
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
69 % this is to draw a gray box around code |
|
70 %(FIXME redefine pagebreak so that it includes a \smallskip) |
|
71 \newenvironment{graybox} |
|
72 {\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\smallskip\FrameRestore}} |
|
73 {\smallskip\endMakeFramed} |
|
74 |
|
75 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
76 % this hack is for getting rid of the ML {* ... *} |
|
77 % scaffolding around function definitions |
|
78 \newenvironment{vanishML}{% |
|
79 \renewcommand{\isacommand}[1]{}% |
|
80 \renewcommand{\isacharverbatimopen}{}% |
|
81 \renewcommand{\isacharverbatimclose}{}}{} |
|
82 |
|
83 \isakeeptag{TutorialML} |
|
84 \renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}} |
|
85 \renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}} |
|
86 |
|
87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
88 % for code that has line numbers |
|
89 \newenvironment{linenos}{\resetlinenumber\internallinenumbers}{\par\nolinenumbers} |
|
90 |
|
91 \isakeeptag{linenos} |
|
92 \renewcommand{\isataglinenos}{\begin{linenos}} |
|
93 \renewcommand{\endisataglinenos}{\end{linenos}} |
|
94 |
|
95 % should only be used in ML code |
|
96 \isakeeptag{linenosgray} |
|
97 \renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}} |
|
98 \renewcommand{\endisataglinenosgray}{\end{linenos}\end{graybox}\end{vanishML}} |
|
99 |
|
100 \isakeeptag{gray} |
|
101 \renewcommand{\isataggray}{\begin{graybox}} |
|
102 \renewcommand{\endisataggray}{\end{graybox}} |
|
103 |
|
104 \isakeeptag{small} |
|
105 \renewcommand{\isatagsmall}{\begingroup\small} |
|
106 \renewcommand{\endisatagsmall}{\endgroup} |
|
107 |
|
108 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
109 \renewenvironment{isabelle} |
|
110 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
|
111 {\end{isabellebody}\end{trivlist}} |
|
112 |
|
113 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
114 % for {* *} in antiquotations |
|
115 \newcommand{\isasymverbopen}{\isacharverbatimopen} |
|
116 \newcommand{\isasymverbclose}{\isacharverbatimclose} |
|
117 |
|
118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
119 % since * cannot be used in text {*...*} |
|
120 \newenvironment{tabularstar}[2] |
|
121 {\begin{tabular*}{#1}{#2}}{\end{tabular*}} |
|
122 |
|
123 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
124 % short hands |
|
125 \def\simpleinductive{\isacommand{simple\isacharunderscore{}inductive}} |
|
126 |
|
127 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
128 \begin{document} |
|
129 |
|
130 \title{\mbox{}\\[-10ex] |
|
131 \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] |
|
132 The Isabelle Programming Tutorial (draft)} |
|
133 |
|
134 \author{by Christian Urban with contributions from:\\[2ex] |
|
135 \begin{tabular}{r@{\hspace{1.8mm}}l} |
|
136 Stefan & Berghofer\\ |
|
137 Sascha & Böhme\\ |
|
138 Jeremy & Dawson\\ |
|
139 Alexander & Krauss\\ |
|
140 \end{tabular}} |
|
141 |
|
142 \maketitle |
|
143 \tableofcontents |
|
144 |
|
145 % generated text of all theories |
|
146 \input{session} |
|
147 |
|
148 \newpage |
|
149 \bibliographystyle{abbrv} |
|
150 \bibliography{root} |
|
151 |
|
152 \end{document} |
|
153 |
|
154 %%% Local Variables: |
|
155 %%% mode: latex |
|
156 %%% TeX-master: t |
|
157 %%% End: |
|