equal
deleted
inserted
replaced
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 {\huge\bf The Isabelle Cookbook}\\ |
155 {\huge\bf The Isabelle Cookbook}\\ |
156 \mbox{A Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)} |
156 \mbox{A Gentle Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)} |
157 |
157 |
158 \author{by Christian Urban with contributions from:\\[2ex] |
158 \author{by Christian Urban with contributions from:\\[2ex] |
159 \begin{tabular}{r@{\hspace{1.8mm}}l} |
159 \begin{tabular}{r@{\hspace{1.8mm}}l} |
160 Stefan & Berghofer\\ |
160 Stefan & Berghofer\\ |
161 Jasmin & Blanchette\\ |
161 Jasmin & Blanchette\\ |