# HG changeset patch
# User nipkow
# Date 1595858323 -7200
# Node ID 1d6c3cba47fec706634ec5a5b7e7cb5266942d91
# Parent  bd9d1ce274c9a911a47c1ea0ef44c755d7f29e37
unclear why I ever asked for type tree2

diff -r bd9d1ce274c9 -r 1d6c3cba47fe 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}