--- a/doc/Contents Tue Jul 30 16:22:39 2013 +0200
+++ b/doc/Contents Tue Jul 30 16:22:39 2013 +0200
@@ -3,6 +3,7 @@
tutorial Tutorial on Isabelle/HOL
locales Tutorial on Locales
classes Tutorial on Type Classes
+ datatypes Tutorial on (Co)datatype Definitions
functions Tutorial on Function Definitions
codegen Tutorial on Code Generation
nitpick User's Guide to Nitpick
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 30 16:22:39 2013 +0200
@@ -0,0 +1,62 @@
+(* Title: Doc/Datatypes/Datatypes.thy
+ Author: Jasmin Blanchette, TU Muenchen
+
+Tutorial for (co)datatype definitions with the new package.
+*)
+
+theory Datatypes
+imports BNF
+begin
+
+section {* Introduction *}
+
+text {*
+ * Isabelle2013 introduced new definitional package for datatypes and codatatypes
+
+ * datatype support is similar to old package, due to Berghofer \& Wenzel \cite{xxx}
+ * indeed, replacing \cmd{datatype} by \cmd{datatype\_new} is usually sufficient
+ to port existing specifications to the new package
+
+ * but it is more powerful, because it is now possible to have nested recursion
+ through a large class of non-datatypes, notably finite sets:
+*}
+
+datatype_new 'a tree = Node 'a "('a tree fset)"
+
+text {*
+ * another advantage: it supports local definitions:
+*}
+
+context linorder
+begin
+
+datatype_new flag = Less | Eq | Greater
+
+end
+
+text {*
+
+ * in a future release, \cmd{datatype\_new} is expected to displace \cmd{datatype}
+
+ *
+*}
+
+section {* Defining Datatypes *}
+
+text {*
+ * theory to include
+*}
+
+section {* Defining Primitive Recursive Functions *}
+
+section {* Defining Codatatypes *}
+
+section {* Defining Primitive Corecursive Functions *}
+
+section {* Registering Bounded Natural Functors *}
+
+section {* Generating Free Constructor Theorems *}
+
+section {* Conclusion *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/document/build Tue Jul 30 16:22:39 2013 +0200
@@ -0,0 +1,14 @@
+#!/bin/bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+cp "$ISABELLE_HOME/src/Doc/iman.sty" .
+cp "$ISABELLE_HOME/src/Doc/extra.sty" .
+cp "$ISABELLE_HOME/src/Doc/isar.sty" .
+cp "$ISABELLE_HOME/src/Doc/manual.bib" .
+
+"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/document/root.tex Tue Jul 30 16:22:39 2013 +0200
@@ -0,0 +1,43 @@
+\documentclass[12pt,a4paper,fleqn]{article}
+\usepackage{latexsym}
+\usepackage{graphicx}
+\usepackage{iman}
+\usepackage{extra}
+\usepackage{isar}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{style}
+\usepackage{pdfsetup}
+
+\newcommand{\cmd}[1]{\isacommand{#1}}
+
+\hyphenation{isa-belle}
+
+\isadroptag{theory}
+
+\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
+Defining (Co)datatypes in Isabelle/HOL}
+\author{\hbox{} \\
+Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel \\
+{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
+\hbox{}}
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+\noindent
+This tutorial describes how to use the new package for defining
+datatypes and codatatypes in Isabelle/HOL. The package provides four
+main user-level commands: \cmd{datatype\_new}, \cmd{codatatype}, \cmd{primrec\_new}, and
+\cmd{primcorec}. The \cmd{\_new} commands are designed to subsume, and eventually
+replace, the corresponding commands from the old datatype package.
+\end{abstract}
+
+\input{Datatypes.tex}
+
+\let\em=\sl
+\bibliography{manual}{}
+\bibliographystyle{abbrv}
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/document/style.sty Tue Jul 30 16:22:39 2013 +0200
@@ -0,0 +1,58 @@
+
+%% toc
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
+\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+
+%% paragraphs
+\setlength{\parindent}{1em}
+
+%% references
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+\newcommand{\ditem}[1]{\item[\isastyletext #1]}
+
+%% quote environment
+\isakeeptag{quote}
+\renewenvironment{quote}
+ {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+ {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
+
+%% typewriter text
+\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
+\renewcommand{\isadigit}[1]{{##1}}%
+\parindent0pt%
+\makeatletter\isa@parindent0pt\makeatother%
+\isabellestyle{tt}\isastyle%
+\fontsize{9pt}{9pt}\selectfont}{}
+
+\isakeeptag{quotetypewriter}
+\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
+\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
+
+%% presentation
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+\binperiod
+\underscoreoff
+
+%% format
+\pagestyle{headings}
+\isabellestyle{it}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "implementation"
+%%% End:
--- a/src/Doc/ROOT Tue Jul 30 16:22:39 2013 +0200
+++ b/src/Doc/ROOT Tue Jul 30 16:22:39 2013 +0200
@@ -37,6 +37,20 @@
"document/root.tex"
"document/style.sty"
+session Datatypes (doc) in "Datatypes" = "HOL-BNF" +
+ options [document_variants = "datatypes"]
+ theories Datatypes
+ files
+ "../prepare_document"
+ "../pdfsetup.sty"
+ "../iman.sty"
+ "../extra.sty"
+ "../isar.sty"
+ "../manual.bib"
+ "document/build"
+ "document/root.tex"
+ "document/style.sty"
+
session Functions (doc) in "Functions" = HOL +
options [document_variants = "functions", skip_proofs = false]
theories Functions