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