src/Doc/Datatypes/Datatypes.thy

 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"
+  "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
 $\lambda$-abstractions and function application rather than through composition.

     record 'a point =
       xval :: 'a
       yval :: 'a
 
 text \<open> \blankline \<close>
-    
+
     copy_bnf ('a, 'z) point_ext
 
 text \<open>
 In the general case, the proof obligations generated by @{command lift_bnf} are
 simpler than the acual BNF properties. In particular, no cardinality reasoning