equal
deleted
inserted
replaced
56 \hyphenation{isa-belle} |
56 \hyphenation{isa-belle} |
57 |
57 |
58 \isadroptag{theory} |
58 \isadroptag{theory} |
59 |
59 |
60 \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] |
60 \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] |
61 Defining (Co)datatypes in Isabelle/HOL} |
61 Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL} |
62 \author{Jasmin Christian Blanchette, |
62 \author{Jasmin Christian Blanchette, |
63 Martin Desharnais, \\ |
63 Martin Desharnais, \\ |
64 Lorenz Panny, |
64 Lorenz Panny, |
65 Andrei Popescu, and |
65 Andrei Popescu, and |
66 Dmitriy Traytel} |
66 Dmitriy Traytel} |
69 |
69 |
70 \begin{document} |
70 \begin{document} |
71 |
71 |
72 \maketitle |
72 \maketitle |
73 |
73 |
|
74 \begin{sloppy} |
74 \begin{abstract} |
75 \begin{abstract} |
75 \noindent |
76 \noindent |
76 This tutorial describes the definitional package for datatypes and codatatypes |
77 This tutorial describes the definitional package for datatypes and codatatypes, |
77 in Isabelle/HOL. The package provides four main commands: \keyw{datatype}, |
78 and for primitively recursive and corecursive functions, in Isabelle/HOL. The |
78 \keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}. |
79 package provides these commands: |
|
80 \keyw{datatype}, \keyw{datatype_compat}, \keyw{primrec}, \keyw{codatatype}, |
|
81 \keyw{primcorec}, \keyw{prim\-co\-recursive}, \keyw{bnf}, \keyw{bnf_axiomatization}, |
|
82 \keyw{print_bnfs}, and \keyw{free_\allowbreak constructors}. |
79 \end{abstract} |
83 \end{abstract} |
|
84 \end{sloppy} |
80 |
85 |
81 \tableofcontents |
86 \tableofcontents |
82 |
87 |
83 \input{Datatypes.tex} |
88 \input{Datatypes.tex} |
84 |
89 |