src/Doc/Datatypes/Datatypes.thy

     primrec_new sum_btree :: "('a\<Colon>plus) btree \<Rightarrow> 'a" where
       "sum_btree (BNode a lt rt) =
          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.
 *}
 
     primrec_new

 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;
+  * and existence of map, set for those
 mention =>.
 *}
 
 
 subsection {* Syntax