# HG changeset patch
# User blanchet
# Date 1455726103 -3600
# Node ID 4a8d2f0d7fdd9c36f22d9a092a1068f05cbda894
# Parent  e85c42f4f30af2b4ccda496e0d8f148e7b3c99fc
tuning

diff -r e85c42f4f30a -r 4a8d2f0d7fdd src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Feb 17 17:08:36 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Feb 17 17:21:43 2016 +0100
@@ -1429,16 +1429,7 @@
 
 text \<open>
 \noindent
-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> list_all (increasing_tree (n + 1)) ts"
-
-text \<open>
-\noindent
-Also for convenience, recursion through functions can also be expressed using
+For convenience, recursion through functions can also be expressed using
 $\lambda$-abstractions and function application rather than through composition.
 For example:
 \<close>
@@ -1478,6 +1469,14 @@
     primrec (nonexhaustive) subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
       "subtree_ft2 x y (FTNode2 g) = g x y"
 
+text \<open>
+For any datatype featuring nesting, 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> list_all (increasing_tree (n + 1)) ts"
+
 
 subsubsection \<open> Nested-as-Mutual Recursion
   \label{sssec:primrec-nested-as-mutual-recursion} \<close>