updated doc
authorblanchet
Mon Oct 21 09:35:18 2013 +0200 (2013-10-21)
changeset 5418166edcd52daeb
parent 54180 1753c57eb16c
child 54182 e3759cbde221
updated doc
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Oct 21 09:31:19 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Oct 21 09:35:18 2013 +0200
     1.3 @@ -1128,20 +1128,14 @@
     1.4  \noindent
     1.5  (No such map function is defined by the package because the type
     1.6  variable @{typ 'a} is dead in @{typ "'a ftree"}.)
     1.7 -
     1.8 -Using \keyw{fun} or \keyw{function}, recursion through functions can be
     1.9 -expressed using $\lambda$-expressions and function application rather
    1.10 -than through composition. For example:
    1.11 +For convenience, recursion through functions can also be expressed using
    1.12 +$\lambda$-expressions and function application rather than through composition.
    1.13 +For example:
    1.14  *}
    1.15  
    1.16 -    datatype_new_compat ftree
    1.17 -
    1.18 -text {* \blankline *}
    1.19 -
    1.20 -    function ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
    1.21 +    primrec_new ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
    1.22        "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
    1.23        "ftree_map f (FTNode g) = FTNode (\<lambda>x. ftree_map f (g x))"
    1.24 -    by auto (metis ftree.exhaust)
    1.25  
    1.26  
    1.27  subsubsection {* Nested-as-Mutual Recursion
    1.28 @@ -1830,8 +1824,8 @@
    1.29  text {*
    1.30  \noindent
    1.31  The map function for the function type (@{text \<Rightarrow>}) is composition
    1.32 -(@{text "op \<circ>"}). For convenience, corecursion through functions can be
    1.33 -expressed using $\lambda$-expressions and function application rather
    1.34 +(@{text "op \<circ>"}). For convenience, corecursion through functions can
    1.35 +also be expressed using $\lambda$-expressions and function application rather
    1.36  than through composition. For example:
    1.37  *}
    1.38