1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Nov 07 00:37:18 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Nov 07 01:01:04 2013 +0100
     1.3 @@ -924,9 +924,9 @@
     1.4  Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
     1.5  new-style datatypes.
     1.6  
     1.7 -\item \emph{Accordingly, the induction principle is different for nested
     1.8 -recursive datatypes.} Again, the old-style induction principle can be generated
     1.9 -on demand using @{command primrec_new}, as explained in
    1.10 +\item \emph{Accordingly, the induction rule is different for nested recursive
    1.11 +datatypes.} Again, the old-style induction rule can be generated on demand using
    1.12 +@{command primrec_new}, as explained in
    1.13  Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
    1.14  new-style datatypes.
    1.15  
    1.16 @@ -1227,12 +1227,12 @@
    1.17  
    1.18  text {*
    1.19  \noindent
    1.20 -Appropriate induction principles are generated under the names
    1.21 +Appropriate induction rules are generated as
    1.22  @{thm [source] at\<^sub>f\<^sub>f.induct},
    1.23  @{thm [source] ats\<^sub>f\<^sub>f.induct}, and
    1.24 -@{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}.
    1.25 -
    1.26 -%%% TODO: Add recursors.
    1.27 +@{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}. The
    1.28 +induction rules and the underlying recursors are generated on a per-need basis
    1.29 +and are kept in a cache to speed up subsequent definitions.
    1.30  
    1.31  Here is a second example:
    1.32  *}
    1.33 @@ -1936,8 +1936,12 @@
    1.34  pretend that nested codatatypes are mutually corecursive. For example:
    1.35  *}
    1.36  
    1.37 +(*<*)
    1.38 +    context late
    1.39 +    begin
    1.40 +(*>*)
    1.41      primcorec
    1.42 -      (*<*)(in late) (*>*)iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and
    1.43 +      iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and
    1.44        iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist"
    1.45      where
    1.46        "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i g (g x))" |
    1.47 @@ -1946,6 +1950,21 @@
    1.48              LNil \<Rightarrow> LNil
    1.49            | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i g x) (iterates\<^sub>i\<^sub>i g xs'))"
    1.50  
    1.51 +text {*
    1.52 +\noindent
    1.53 +Coinduction rules are generated as
    1.54 +@{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
    1.55 +@{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
    1.56 +@{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
    1.57 +and analogously for @{text strong_coinduct}. These rules and the
    1.58 +underlying corecursors are generated on a per-need basis and are kept in a cache
    1.59 +to speed up subsequent definitions.
    1.60 +*}
    1.61 +
    1.62 +(*<*)
    1.63 +    end
    1.64 +(*>*)
    1.65 +
    1.66  
    1.67  subsubsection {* Constructor View
    1.68    \label{ssec:primrec-constructor-view} *}