author | blanchet |
Mon, 05 Jan 2015 11:00:12 +0100 | |
changeset 59282 | c5f6e2c4472c |
parent 58310 | 91ea607a34d8 |
child 59300 | 7009e5fa5cd3 |
permissions | -rw-r--r-- |
52794 | 1 |
\documentclass[12pt,a4paper]{article} % fleqn |
55290 | 2 |
\usepackage[T1]{fontenc} |
55355 | 3 |
\usepackage{amsmath} |
52805 | 4 |
\usepackage{cite} |
5 |
\usepackage{enumitem} |
|
53647 | 6 |
\usepackage{footmisc} |
52792 | 7 |
\usepackage{latexsym} |
8 |
\usepackage{graphicx} |
|
9 |
\usepackage{iman} |
|
10 |
\usepackage{extra} |
|
11 |
\usepackage{isar} |
|
12 |
\usepackage{isabelle} |
|
13 |
\usepackage{isabellesym} |
|
14 |
\usepackage{style} |
|
15 |
\usepackage{pdfsetup} |
|
52822 | 16 |
\usepackage{railsetup} |
17 |
\usepackage{framed} |
|
57542 | 18 |
\usepackage{regexpatch} |
19 |
||
20 |
\makeatletter |
|
21 |
\xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}% |
|
22 |
\xpatchcmd{\sectionmark}{\MakeUppercase}{}{}{}% |
|
23 |
\xpatchcmd*{\tableofcontents}{\MakeUppercase}{}{}{}% |
|
24 |
\makeatother |
|
52792 | 25 |
|
53552 | 26 |
\setcounter{secnumdepth}{3} |
27 |
\setcounter{tocdepth}{3} |
|
28 |
||
55290 | 29 |
\renewcommand\_{\hbox{\textunderscore\kern-.05ex}} |
30 |
||
52805 | 31 |
\newbox\boxA |
32 |
\setbox\boxA=\hbox{\ } |
|
33 |
\parindent=4\wd\boxA |
|
34 |
||
53621 | 35 |
\newcommand\blankline{\vskip-.25\baselineskip} |
53552 | 36 |
|
53621 | 37 |
\newenvironment{indentblock}{\list{}{\setlength{\leftmargin}{\parindent}}\item[]}{\endlist} |
53552 | 38 |
|
53617 | 39 |
\newcommand{\keyw}[1]{\textbf{#1}} |
53534 | 40 |
\newcommand{\synt}[1]{\textit{#1}} |
53544 | 41 |
\newcommand{\hthm}[1]{\textbf{\textit{#1}}} |
52792 | 42 |
|
53491 | 43 |
%\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$} |
55355 | 44 |
\renewcommand\isactrlsub[1]{\/$\sb{#1}$} |
45 |
\renewcommand\isadigit[1]{\/\ensuremath{\mathrm{#1}}} |
|
46 |
\renewcommand\isacharprime{\isamath{{'}\mskip-2mu}} |
|
47 |
\renewcommand\isacharunderscore{\mbox{\_}} |
|
48 |
\renewcommand\isacharunderscorekeyword{\mbox{\_}} |
|
49 |
\renewcommand\isachardoublequote{\mbox{\upshape{``}}} |
|
50 |
\renewcommand\isachardoublequoteopen{\mbox{\upshape{``}\kern.1ex}} |
|
51 |
\renewcommand\isachardoublequoteclose{\/\kern.15ex\mbox{\upshape{''}}} |
|
52 |
\renewcommand\isacharverbatimopen{\isacharbraceleft\isacharasterisk} |
|
53 |
\renewcommand\isacharverbatimclose{\isacharasterisk\isacharbraceright} |
|
57575 | 54 |
\renewcommand{\isasyminverse}{\isamath{{}^{-}}} |
52794 | 55 |
|
52792 | 56 |
\hyphenation{isa-belle} |
57 |
||
58 |
\isadroptag{theory} |
|
59 |
||
60 |
\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] |
|
61 |
Defining (Co)datatypes in Isabelle/HOL} |
|
59282 | 62 |
\author{Jasmin Christian Blanchette, |
57079 | 63 |
Martin Desharnais, \\ |
64 |
Lorenz Panny, |
|
53619 | 65 |
Andrei Popescu, and |
59282 | 66 |
Dmitriy Traytel} |
55290 | 67 |
|
68 |
\urlstyle{tt} |
|
69 |
||
52792 | 70 |
\begin{document} |
71 |
||
72 |
\maketitle |
|
73 |
||
74 |
\begin{abstract} |
|
75 |
\noindent |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
57575
diff
changeset
|
76 |
This tutorial describes the definitional package for datatypes and codatatypes |
58310 | 77 |
in Isabelle/HOL. The package provides four main commands: \keyw{datatype}, |
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
57575
diff
changeset
|
78 |
\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}. |
52792 | 79 |
\end{abstract} |
80 |
||
52794 | 81 |
\tableofcontents |
82 |
||
52792 | 83 |
\input{Datatypes.tex} |
84 |
||
85 |
\let\em=\sl |
|
86 |
\bibliography{manual}{} |
|
87 |
\bibliographystyle{abbrv} |
|
88 |
||
89 |
\end{document} |