equal
deleted
inserted
replaced
|
1 \documentclass[12pt,a4paper,fleqn]{article} |
|
2 \usepackage{latexsym} |
|
3 \usepackage{graphicx} |
|
4 \usepackage{iman} |
|
5 \usepackage{extra} |
|
6 \usepackage{isar} |
|
7 \usepackage{isabelle} |
|
8 \usepackage{isabellesym} |
|
9 \usepackage{style} |
|
10 \usepackage{pdfsetup} |
|
11 |
|
12 \newcommand{\cmd}[1]{\isacommand{#1}} |
|
13 |
|
14 \hyphenation{isa-belle} |
|
15 |
|
16 \isadroptag{theory} |
|
17 |
|
18 \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] |
|
19 Defining (Co)datatypes in Isabelle/HOL} |
|
20 \author{\hbox{} \\ |
|
21 Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel \\ |
|
22 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ |
|
23 \hbox{}} |
|
24 \begin{document} |
|
25 |
|
26 \maketitle |
|
27 |
|
28 \begin{abstract} |
|
29 \noindent |
|
30 This tutorial describes how to use the new package for defining |
|
31 datatypes and codatatypes in Isabelle/HOL. The package provides four |
|
32 main user-level commands: \cmd{datatype\_new}, \cmd{codatatype}, \cmd{primrec\_new}, and |
|
33 \cmd{primcorec}. The \cmd{\_new} commands are designed to subsume, and eventually |
|
34 replace, the corresponding commands from the old datatype package. |
|
35 \end{abstract} |
|
36 |
|
37 \input{Datatypes.tex} |
|
38 |
|
39 \let\em=\sl |
|
40 \bibliography{manual}{} |
|
41 \bibliographystyle{abbrv} |
|
42 |
|
43 \end{document} |