17 \setbox\boxA=\hbox{\ } |
17 \setbox\boxA=\hbox{\ } |
18 \parindent=4\wd\boxA |
18 \parindent=4\wd\boxA |
19 |
19 |
20 \newcommand{\keyw}[1]{\isacommand{#1}} |
20 \newcommand{\keyw}[1]{\isacommand{#1}} |
21 |
21 |
|
22 \renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$} |
22 \renewcommand{\isacharprime}{\isamath{{'}\mskip-2mu}} |
23 \renewcommand{\isacharprime}{\isamath{{'}\mskip-2mu}} |
23 \renewcommand{\isacharunderscore}{\mbox{\_}} |
24 \renewcommand{\isacharunderscore}{\mbox{\_}} |
24 \renewcommand{\isacharunderscorekeyword}{\mbox{\_}} |
25 \renewcommand{\isacharunderscorekeyword}{\mbox{\_}} |
25 \renewcommand{\isachardoublequote}{\mbox{\upshape{``}}} |
26 \renewcommand{\isachardoublequote}{\mbox{\upshape{``}}} |
26 \renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\kern.05ex}} |
27 \renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\kern.1ex}} |
27 \renewcommand{\isachardoublequoteclose}{\/\kern.1ex\mbox{\upshape{''}}} |
28 \renewcommand{\isachardoublequoteclose}{\/\kern.15ex\mbox{\upshape{''}}} |
28 |
29 |
29 \hyphenation{isa-belle} |
30 \hyphenation{isa-belle} |
30 |
31 |
31 \isadroptag{theory} |
32 \isadroptag{theory} |
32 |
33 |
33 \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] |
34 \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] |
34 Defining (Co)datatypes in Isabelle/HOL} |
35 Defining (Co)datatypes in Isabelle/HOL} |
35 \author{\hbox{} \\ |
36 \author{\hbox{} \\ |
36 Jasmin Christian Blanchette \\ |
37 Jasmin Christian Blanchette \\ |
|
38 Lorenz Panny \\ |
37 Andrei Popescu \\ |
39 Andrei Popescu \\ |
38 Dmitriy Traytel \\ |
40 Dmitriy Traytel \\ |
39 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ |
41 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ |
40 \hbox{}} |
42 \hbox{}} |
41 \begin{document} |
43 \begin{document} |