equal
deleted
inserted
replaced
144 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
144 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
145 {\end{isabellebody}\end{trivlist}} |
145 {\end{isabellebody}\end{trivlist}} |
146 |
146 |
147 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
147 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
148 % for {* *} in antiquotations |
148 % for {* *} in antiquotations |
149 \newcommand{\isasymverbopen}{\isacharverbatimopen} |
149 %\newcommand{\isasymverbopen}{\isacharverbatimopen} |
150 \newcommand{\isasymverbclose}{\isacharverbatimclose} |
150 %\newcommand{\isasymverbclose}{\isacharverbatimclose} |
|
151 \newcommand{\isasymverbopen}{\isacartoucheopen} |
|
152 \newcommand{\isasymverbclose}{\isacartoucheclose} |
151 \newcommand{\isasymfoo}{\isa{{\isacharbackslash}{\isacharless}foo{\isachargreater}}} |
153 \newcommand{\isasymfoo}{\isa{{\isacharbackslash}{\isacharless}foo{\isachargreater}}} |
152 |
154 |
153 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
155 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
154 % since * cannot be used in text {*...*} |
156 % since * cannot be used in text {*...*} |
155 \newenvironment{tabularstar}[2] |
157 \newenvironment{tabularstar}[2] |
163 \begin{document} |
165 \begin{document} |
164 |
166 |
165 \title{\mbox{}\\[-10ex] |
167 \title{\mbox{}\\[-10ex] |
166 \includegraphics[scale=0.5]{tutorial-logo.jpg}\\[3ex] |
168 \includegraphics[scale=0.5]{tutorial-logo.jpg}\\[3ex] |
167 {\huge\bf The Isabelle Cookbook}\\ |
169 {\huge\bf The Isabelle Cookbook}\\ |
168 \mbox{A Gentle Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)} |
170 \mbox{A Gentle Tutorial for Programming Isabelle/ML}\\ (draft)} |
169 |
171 |
170 \author{by Christian Urban with contributions from:\\[2ex] |
172 \author{by Christian Urban with contributions from:\\[2ex] |
171 \begin{tabular}{r@{\hspace{1.8mm}}l} |
173 \begin{tabular}{r@{\hspace{1.8mm}}l} |
172 Stefan & Berghofer\\ |
174 Stefan & Berghofer\\ |
173 Jasmin & Blanchette\\ |
175 Jasmin & Blanchette\\ |
175 Lukas & Bulwahn\\ |
177 Lukas & Bulwahn\\ |
176 Jeremy & Dawson\\ |
178 Jeremy & Dawson\\ |
177 Rafal & Kolanski\\ |
179 Rafal & Kolanski\\ |
178 Alexander & Krauss\\ |
180 Alexander & Krauss\\ |
179 Tobias & Nipkow\\ |
181 Tobias & Nipkow\\ |
|
182 Norbert & Schirmer\\ |
180 Andreas & Schropp\\ |
183 Andreas & Schropp\\ |
181 Christian & Sternagel\\ |
184 Christian & Sternagel\\ |
182 \end{tabular}} |
185 \end{tabular}} |
183 |
186 |
184 \maketitle |
187 \maketitle |