# HG changeset patch
# User blanchet
# Date 1377153747 -7200
# Node ID 98a2c33d5d1b36f87f6b3d773808065ed85d939c
# Parent  f08f66b55cb5d711680c3dfd25958a2043a9eff1
ideas for (co)datatype docs

diff -r f08f66b55cb5 -r 98a2c33d5d1b src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Aug 22 08:42:27 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Aug 22 08:42:27 2013 +0200
@@ -729,11 +729,14 @@
          a + the_default Zero (option_map sum_btree lt) +
            the_default Zero (option_map sum_btree rt)"
 
+text {*
+Show example with function composition (ftree).
+*}
 
 subsubsection {* Nested-as-Mutual Recursion *}
 
 text {*
-  * can pretend a nested type is mutually recursive
+  * can pretend a nested type is mutually recursive (if purely inductive)
   * avoids the higher-order map
   * e.g.
 *}
@@ -994,6 +997,7 @@
 \verb|~~/src/HOL/BNF/More_BNFs.thy|.
 
 Mention distinction between live and dead type arguments;
+  * and existence of map, set for those
 mention =>.
 *}