src/Doc/Datatypes/Datatypes.thy

 \cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
 @{command datatype_new} is usually all that is needed to port existing theories
 to use the new package.
 
 Perhaps the main advantage of the new package is that it supports recursion
-through a large class of non-datatypes, comprising finite sets:
+through a large class of non-datatypes, such as finite sets:
 *}
 
     datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s 'a "'a tree\<^sub>f\<^sub>s fset"
 
 text {*

   @{syntax_def primrec_equation}: thmdecl? prop
 "}
 *}
 
 
+(*
 subsection {* Generated Theorems
   \label{ssec:primrec-generated-theorems} *}
 
 text {*
 %  * synthesized nonrecursive definition

 %    * mutualized
 %    * without some needless induction hypotheses if not used
 %  * fold, rec
 %    * mutualized
 *}
+*)
+
 
 subsection {* Recursive Default Values for Selectors
   \label{ssec:recursive-default-values-for-selectors} *}
 
 text {*

 \item
 Derive the desired equation on @{text un_D} from the characteristic equations
 for @{text "un_D\<^sub>0"}.
 \end{enumerate}
 
+\noindent
 The following example illustrates this procedure:
 *}
 
     consts termi\<^sub>0 :: 'a
+
+text {* \blankline *}
 
     datatype_new ('a, 'b) tlist =
       TNil (termi: 'b) (defaults ttl: TNil)
     | TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
+
+text {* \blankline *}
 
     overloading
       termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
     begin
     primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
     "termi\<^sub>0 (TNil y) = y" |
     "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
     end
 
+text {* \blankline *}
+
     lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs"
     by (cases xs) auto
 
 
 (*

 
 section {* Defining Codatatypes
   \label{sec:defining-codatatypes} *}
 
 text {*
-This section describes how to specify codatatypes using the @{command codatatype}
-command.
-
-%  * libraries include some useful codatatypes, notably lazy lists;
-%    see the ``Coinductive'' AFP entry \cite{xxx} for an elaborate library
-*}
-
-
+This section describes how to specify codatatypes using the @{command
+codatatype} command. The command is first illustrated through concrete examples
+featuring different flavors of corecursion. More examples can be found in the
+directory \verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs}
+also includes some useful codatatypes, notably for lazy lists
+\cite{lochbihler-2010}.
+*}
+
+
+(*
 subsection {* Introductory Examples
   \label{ssec:codatatype-introductory-examples} *}
 
 text {*
 More examples in \verb|~~/src/HOL/BNF/Examples|.
 *}
+*)
 
 
 subsection {* Command Syntax
   \label{ssec:codatatype-command-syntax} *}
+
+
+subsubsection {* \keyw{codatatype} *}
 
 text {*
 Definitions of codatatypes have almost exactly the same syntax as for datatypes
 (Section~\ref{ssec:datatype-command-syntax}), with two exceptions: The command
 is called @{command codatatype}; the \keyw{no\_discs\_sels} option is not
 available, because destructors are a central notion for codatatypes.
 *}
 
 
+(*
 subsection {* Generated Constants
   \label{ssec:codatatype-generated-constants} *}
-
-
+*)
+
+
+(*
 subsection {* Generated Theorems
   \label{ssec:codatatype-generated-theorems} *}
+*)
 
 
 section {* Defining Corecursive Functions
   \label{sec:defining-corecursive-functions} *}
 

 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy
 %%% lists (cf. terminal0 in TLList.thy)
 *}
 
 
+(*
 subsection {* Introductory Examples
   \label{ssec:primcorec-introductory-examples} *}
 
 text {*
 More examples in \verb|~~/src/HOL/BNF/Examples|.
 
 Also, for default values, the same trick as for datatypes is possible for
 codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}).
 *}
+*)
 
 
 subsection {* Command Syntax
   \label{ssec:primcorec-command-syntax} *}
 

   @{syntax_def primcorec_formula}: thmdecl? prop (@'of' (term * ))?
 "}
 *}
 
 
+(*
 subsection {* Generated Theorems
   \label{ssec:primcorec-generated-theorems} *}
+*)
 
 
 section {* Registering Bounded Natural Functors
   \label{sec:registering-bounded-natural-functors} *}
 

 of a bounded natural functor (BNF).
 
 *}
 
 
+(*
 subsection {* Introductory Example
   \label{ssec:bnf-introductory-example} *}
 
 text {*
 More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and

 
 %Mention distinction between live and dead type arguments;
 %  * and existence of map, set for those
 %mention =>.
 *}
+*)
 
 
 subsection {* Command Syntax
   \label{ssec:bnf-command-syntax} *}
 

   @@{command_def bnf} target? (name ':')? term \\
     term_list term term_list term?
   ;
   X_list: '[' (X + ',') ']'
 "}
-
-options: no_discs_sels rep_compat
 *}
 
 
 subsubsection {* \keyw{print\_bnfs} *}
 

 %    * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
 %    * hack to have both co and nonco view via locale (cf. ext nats)
 *}
 
 
+(*
 subsection {* Introductory Example
   \label{ssec:ctors-introductory-example} *}
+*)
 
 
 subsection {* Command Syntax
   \label{ssec:ctors-command-syntax} *}
 

 %
 %* issues with HOL-Proofs?
 %
 %* partial documentation
 %
-%* too much output by commands like "datatype_new" and "codatatype"
-%
-%* no direct way to define recursive functions for default values -- but show trick
-%  based on overloading
-%
 %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
 %  (for @{command datatype_new_compat} and prim(co)rec)
 %
-%* no way to register same type as both data- and codatatype?
+%    * a fortiori, no way to register same type as both data- and codatatype
 %
 %* no recursion through unused arguments (unlike with the old package)
 %
 %* in a locale, cannot use locally fixed types (because of limitation in typedef)?
+%
+% *names of variables suboptimal
 *}
 
 
 section {* Acknowledgments
   \label{sec:acknowledgments} *}