--- a/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 15:41:28 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 16:26:50 2016 +0100
@@ -1434,7 +1434,7 @@
\<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"
+ "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
@@ -2922,7 +2922,7 @@
yval :: 'a
text \<open> \blankline \<close>
-
+
copy_bnf ('a, 'z) point_ext
text \<open>