1\documentclass[12pt,a4paper]{article} % fleqn
2\usepackage{lmodern}
3\usepackage[T1]{fontenc}
4\usepackage{amsfonts}
5\usepackage{amsmath}
6\usepackage{cite}
7\usepackage{enumitem}
8\usepackage{footmisc}
9\usepackage{latexsym}
10\usepackage{graphicx}
11\usepackage{iman}
12\usepackage{extra}
13\usepackage{isar}
14\usepackage{isabelle}
15\usepackage{isabellesym}
16\usepackage{style}
17\usepackage{pdfsetup}
18\usepackage{railsetup}
19\usepackage{framed}
20\usepackage{regexpatch}
21
22\makeatletter
23\xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}%
24\xpatchcmd{\sectionmark}{\MakeUppercase}{}{}{}%
25\xpatchcmd*{\tableofcontents}{\MakeUppercase}{}{}{}%
26\makeatother
27
28\setcounter{secnumdepth}{3}
29\setcounter{tocdepth}{3}
30
31\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
32
33\newbox\boxA
34\setbox\boxA=\hbox{\ }
35\parindent=4\wd\boxA
36
37\newcommand\blankline{\vskip-.25\baselineskip}
38
39\newenvironment{indentblock}{\list{}{\setlength{\leftmargin}{\parindent}}\item[]}{\endlist}
40
41\newcommand{\keyw}[1]{\textbf{#1}}
42\newcommand{\synt}[1]{\textit{#1}}
43\newcommand{\hthm}[1]{\textbf{\textit{#1}}}
44
45%\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
46\renewcommand\isactrlsub[1]{\/$\sb{#1}$}
47\renewcommand\isadigit[1]{\/\ensuremath{\mathrm{#1}}}
48\renewcommand\isacharprime{\isamath{{'}\mskip-2mu}}
49\renewcommand\isacharunderscore{\mbox{\_}}
50\renewcommand\isacharunderscorekeyword{\mbox{\_}}
51\renewcommand\isachardoublequote{\mbox{\upshape{``}}}
52\renewcommand\isachardoublequoteopen{\mbox{\upshape{``}\kern.1ex}}
53\renewcommand\isachardoublequoteclose{\/\kern.15ex\mbox{\upshape{''}}}
54\renewcommand\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
55\renewcommand\isacharverbatimclose{\isacharasterisk\isacharbraceright}
56\renewcommand{\isasyminverse}{\isamath{{}^{-}}}
57
58\hyphenation{isa-belle}
59
60\isadroptag{theory}
61
62\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
63Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}
64\author{Julian Biendarra, Jasmin Christian Blanchette, \\
65Martin Desharnais, Lorenz Panny, \\
66Andrei Popescu, and Dmitriy Traytel}
67
68\urlstyle{tt}
69
70\begin{document}
71
72\maketitle
73
74\begin{sloppy}
75\begin{abstract}
76\noindent
77This tutorial describes the definitional package for datatypes and codatatypes,
78and for primitively recursive and corecursive functions, in Isabelle/HOL. The
79following commands are provided:
80\keyw{datatype}, \keyw{datatype_\allowbreak compat}, \keyw{prim\-rec}, \keyw{co\-data\-type},
81\keyw{prim\-co\-rec}, \keyw{prim\-co\-recursive}, \keyw{bnf}, \keyw{lift_\allowbreak bnf},
82\keyw{copy_\allowbreak bnf}, \keyw{bnf_\allowbreak axiom\-atization},
83\keyw{print_\allowbreak bnfs}, and \keyw{free_\allowbreak constructors}.
84\end{abstract}
85\end{sloppy}
86
87\tableofcontents
88
89\input{Datatypes.tex}
90
91\let\em=\sl
92\bibliography{manual}{}
93\bibliographystyle{abbrv}
94
95\end{document}
96