# HG changeset patch
# User traytel
# Date 1455722810 -3600
# Node ID e4e09a6e3922cb408ffb989939935babd60371ea
# Parent  eeaa2f7b53296f685e0cf1e95d76ceda3435e891
adjust 112eefe85ff0 to 532ad8de5d61

diff -r eeaa2f7b5329 -r e4e09a6e3922 src/Doc/Datatypes/Datatypes.thy
--- 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>