unclear why I ever asked for type tree2
authornipkow
Mon, 27 Jul 2020 15:58:43 +0200
changeset 72307 1d6c3cba47fe
parent 72306 bd9d1ce274c9
child 72308 b8d0b8659e0a
unclear why I ever asked for type tree2
src/Doc/Prog_Prove/Types_and_funs.thy
--- 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 @@
 \end{exercise}
 
 \begin{exercise}
-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>.
 \end{exercise}