# HG changeset patch
# User blanchet
# Date 1375270857 -7200
# Node ID 146ce45c36198a49933bd2202d220ce54169c74b
# Parent  7f2f420463614617581c517e3d954e53e25ad518
more work on (co)datatype docs

diff -r 7f2f42046361 -r 146ce45c3619 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Jul 31 11:28:59 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Jul 31 13:40:57 2013 +0200
@@ -72,11 +72,14 @@
 
 text {*
 To use the package, it is necessary to import the @{theory BNF} theory, which
-can be precompiled as the \textit{HOL-BNF} image:
+can be precompiled as the \textit{HOL-BNF} image. The following commands show
+how to launch jEdit/PIDE with the image loaded and how to build the image
+without launching jEdit:
 *}
 
 text {*
 \noindent
+\ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\
 \ \ \ \ \texttt{isabelle build -b HOL-BNF}
 *}
 
@@ -200,7 +203,7 @@
 *}
 
     datatype_new ('a, 'b) expr =
-      Term "('a, 'b) term" | Sum "('a, 'b) term" "('a, 'b) expr"
+      Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) expr"
     and ('a, 'b) trm =
       Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
     and ('a, 'b) factor =
@@ -227,6 +230,18 @@
     datatype_new 'a foo = Foo (*<*) datatype_new 'a bar = Bar  "'a foo \<Rightarrow> 'a foo"
 *)
 
+    datatype_new 'a evil = Evil (*<*)'a
+    typ (*>*)"'a evil \<Rightarrow> 'a evil"
+
+text {*
+Issue: => allows recursion only on its right-hand side.
+This issue is inherited by polymorphic datatypes (and codatatypes)
+defined in terms of =>.
+In general, type constructors "('a1, ..., 'an) k" allow recursion on a subset
+of their type arguments.
+*}
+
+
 subsubsection {* Auxiliary Constants and Syntaxes *}
 
 text {*
@@ -318,6 +333,9 @@
 text {*
 More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
 \verb|~~/src/HOL/BNF/More_BNFs.thy|.
+
+Mention distinction between live and dead type arguments;
+mention =>.
 *}
 
 subsection {* General Syntax *}
@@ -378,7 +396,15 @@
 *}
 
 text {*
+* primrec\_new and primcorec are vaporware
+
 * slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
+
+* issues with HOL-Proofs?
+
+* partial documentation
+
+* too much output by commands like "datatype_new" and "codatatype"
 *}
 
 end
diff -r 7f2f42046361 -r 146ce45c3619 src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Wed Jul 31 11:28:59 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Wed Jul 31 13:40:57 2013 +0200
@@ -17,11 +17,12 @@
 
 \newcommand{\cmd}[1]{\isacommand{#1}}
 
+\def\isacharprime{\isamath{{'}\mskip-2mu}}
 \renewcommand{\isacharunderscore}{\mbox{\_}}
 \renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
 \renewcommand{\isachardoublequote}{\mbox{\upshape{``}}}
-\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}}}
-\renewcommand{\isachardoublequoteclose}{\mbox{\upshape{''}}}
+\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\,}}
+\renewcommand{\isachardoublequoteclose}{\mbox{\,\upshape{''}}}
 
 \hyphenation{isa-belle}