src/Doc/Datatypes/Datatypes.thy
changeset 62333 e4e09a6e3922
parent 62331 e923f200bda5
child 62336 4a8d2f0d7fdd
--- 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>