src/Doc/Datatypes/document/root.tex
author blanchet
Wed Sep 11 18:32:43 2013 +0200 (2013-09-11)
changeset 53544 2176a7e40786
parent 53534 de2027f9aff3
child 53552 eed6efba4e3f
permissions -rw-r--r--
more (co)data docs
blanchet@52794
     1
\documentclass[12pt,a4paper]{article} % fleqn
blanchet@52805
     2
\usepackage{cite}
blanchet@52805
     3
\usepackage{enumitem}
blanchet@52792
     4
\usepackage{latexsym}
blanchet@52792
     5
\usepackage{graphicx}
blanchet@52792
     6
\usepackage{iman}
blanchet@52792
     7
\usepackage{extra}
blanchet@52792
     8
\usepackage{isar}
blanchet@52792
     9
\usepackage{isabelle}
blanchet@52792
    10
\usepackage{isabellesym}
blanchet@52792
    11
\usepackage{style}
blanchet@52792
    12
\usepackage{pdfsetup}
blanchet@52822
    13
\usepackage{railsetup}
blanchet@52822
    14
\usepackage{framed}
blanchet@52792
    15
blanchet@52805
    16
\newbox\boxA
blanchet@52805
    17
\setbox\boxA=\hbox{\ }
blanchet@52805
    18
\parindent=4\wd\boxA
blanchet@52805
    19
blanchet@52824
    20
\newcommand{\keyw}[1]{\isacommand{#1}}
blanchet@53534
    21
\newcommand{\synt}[1]{\textit{#1}}
blanchet@53544
    22
\newcommand{\hthm}[1]{\textbf{\textit{#1}}}
blanchet@52792
    23
blanchet@53491
    24
%\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
blanchet@53491
    25
\renewcommand{\isactrlsub}[1]{\/$\sb{#1}$}
blanchet@53491
    26
\renewcommand{\isadigit}[1]{\/\ensuremath{\mathrm{#1}}}
blanchet@52822
    27
\renewcommand{\isacharprime}{\isamath{{'}\mskip-2mu}}
blanchet@52794
    28
\renewcommand{\isacharunderscore}{\mbox{\_}}
blanchet@52794
    29
\renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
blanchet@52805
    30
\renewcommand{\isachardoublequote}{\mbox{\upshape{``}}}
blanchet@53028
    31
\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\kern.1ex}}
blanchet@53028
    32
\renewcommand{\isachardoublequoteclose}{\/\kern.15ex\mbox{\upshape{''}}}
blanchet@52794
    33
blanchet@52792
    34
\hyphenation{isa-belle}
blanchet@52792
    35
blanchet@52792
    36
\isadroptag{theory}
blanchet@52792
    37
blanchet@52792
    38
\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
blanchet@52792
    39
Defining (Co)datatypes in Isabelle/HOL}
blanchet@52792
    40
\author{\hbox{} \\
blanchet@52805
    41
Jasmin Christian Blanchette \\
blanchet@53028
    42
Lorenz Panny \\
blanchet@52805
    43
Andrei Popescu \\
blanchet@52805
    44
Dmitriy Traytel \\
blanchet@52792
    45
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
blanchet@52792
    46
\hbox{}}
blanchet@52792
    47
\begin{document}
blanchet@52792
    48
blanchet@52792
    49
\maketitle
blanchet@52792
    50
blanchet@52792
    51
\begin{abstract}
blanchet@52792
    52
\noindent
blanchet@52794
    53
This tutorial describes how to use the new package for defining datatypes and
blanchet@52794
    54
codatatypes in Isabelle/HOL. The package provides four main user-level commands:
blanchet@52824
    55
\keyw{datatype\_new}, \keyw{codatatype}, \keyw{primrec\_new}, and \keyw{primcorec}.
blanchet@52824
    56
The commands suffixed by \keyw{\_new} are intended to subsume, and eventually
blanchet@52792
    57
replace, the corresponding commands from the old datatype package.
blanchet@52792
    58
\end{abstract}
blanchet@52792
    59
blanchet@52794
    60
\tableofcontents
blanchet@52794
    61
blanchet@52792
    62
\input{Datatypes.tex}
blanchet@52792
    63
blanchet@52792
    64
\let\em=\sl
blanchet@52792
    65
\bibliography{manual}{}
blanchet@52792
    66
\bibliographystyle{abbrv}
blanchet@52792
    67
blanchet@52792
    68
\end{document}