--- a/NEWS Wed Feb 17 11:54:34 2016 +0100
+++ b/NEWS Wed Feb 17 12:07:49 2016 +0100
@@ -13,6 +13,13 @@
typesetting. E.g. to produce proof holes in examples and documentation.
+*** HOL ***
+
+* (Co)datatype package:
+ - "primrec" now allows nested calls through the predicator in addition
+ to the map function.
+
+
New in Isabelle2016 (February 2016)
-----------------------------------
--- a/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 11:54:34 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 12:07:49 2016 +0100
@@ -1392,7 +1392,16 @@
text \<open>
\noindent
-For convenience, recursion through functions can also be expressed using
+For convenience, the predicator can be used instead of the map function,
+typically when defining predicates. For example:
+\<close>
+
+primrec increasing_tree :: "int \<Rightarrow> int tree\<^sub>f\<^sub>f \<Rightarrow> bool" where
+ "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow> n \<ge> m \<and> pred_list (increasing_tree (n + 1)) ts"
+
+text \<open>
+\noindent
+Also for convenience, recursion through functions can also be expressed using
$\lambda$-abstractions and function application rather than through composition.
For example:
\<close>