changeset 72307 1d6c3cba47fe
parent 69609 ff784d5a5bfb
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Sun Jul 26 22:28:43 2020 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Mon Jul 27 15:58:43 2020 +0200
@@ -224,10 +224,8 @@
-Define a new type \<open>'a tree2\<close> of binary trees where values are also
-stored in the leaves of the tree.  Also reformulate the
-\<^const>\<open>mirror\<close> function accordingly. Define two functions
-\<open>pre_order\<close> and \<open>post_order\<close> of type \<open>'a tree2 \<Rightarrow> 'a list\<close>
+Define the two functions
+\<open>pre_order\<close> and \<open>post_order\<close> of type @{typ "'a tree \<Rightarrow> 'a list"}
 that traverse a tree and collect all stored values in the respective order in
 a list. Prove \<^prop>\<open>pre_order (mirror t) = rev (post_order t)\<close>.