# HG changeset patch
# User blanchet
# Date 1455707269 -3600
# Node ID 112eefe85ff03a829190f2487c4f95c5b32ac1bf
# Parent  3cf7a067599c2641851a76add599d0780596feae
document new 'primrec' feature

diff -r 3cf7a067599c -r 112eefe85ff0 NEWS
--- 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)
 -----------------------------------
 
diff -r 3cf7a067599c -r 112eefe85ff0 src/Doc/Datatypes/Datatypes.thy
--- 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>