equal
deleted
inserted
replaced
150 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
150 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
151 \begin{document} |
151 \begin{document} |
152 |
152 |
153 \title{\mbox{}\\[-10ex] |
153 \title{\mbox{}\\[-10ex] |
154 \includegraphics[scale=0.5]{tutorial-logo.jpg}\\[3ex] |
154 \includegraphics[scale=0.5]{tutorial-logo.jpg}\\[3ex] |
155 The Isabelle Programming Tutorial (draft)} |
155 {\huge\bf The Isabelle Cookbook}\\ |
|
156 \mbox{A Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)} |
156 |
157 |
157 \author{by Christian Urban with contributions from:\\[2ex] |
158 \author{by Christian Urban with contributions from:\\[2ex] |
158 \begin{tabular}{r@{\hspace{1.8mm}}l} |
159 \begin{tabular}{r@{\hspace{1.8mm}}l} |
159 Stefan & Berghofer\\ |
160 Stefan & Berghofer\\ |
160 Jasmin & Blanchette\\ |
161 Jasmin & Blanchette\\ |
161 Sascha & Böhme\\ |
162 Sascha & Böhme\\ |
162 Lukas & Bulwahn\\ |
163 Lukas & Bulwahn\\ |
163 Jeremy & Dawson\\ |
164 Jeremy & Dawson\\ |
164 Alexander & Krauss\\ |
165 Alexander & Krauss\\ |
|
166 Tobias & Nipkow\\ |
165 Christian & Sternagel\\ |
167 Christian & Sternagel\\ |
166 \end{tabular}} |
168 \end{tabular}} |
167 |
169 |
168 \maketitle |
170 \maketitle |
169 |
171 |