unclear why I ever asked for type tree2
authornipkow
Mon Jul 27 15:58:43 2020 +0200 (2 weeks ago)
changeset 720771d6c3cba47fe
parent 72076 bd9d1ce274c9
child 72078 b8d0b8659e0a
unclear why I ever asked for type tree2
src/Doc/Prog_Prove/Types_and_funs.thy
     1.1 --- a/src/Doc/Prog_Prove/Types_and_funs.thy	Sun Jul 26 22:28:43 2020 +0200
     1.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Mon Jul 27 15:58:43 2020 +0200
     1.3 @@ -224,10 +224,8 @@
     1.4  \end{exercise}
     1.5  
     1.6  \begin{exercise}
     1.7 -Define a new type \<open>'a tree2\<close> of binary trees where values are also
     1.8 -stored in the leaves of the tree.  Also reformulate the
     1.9 -\<^const>\<open>mirror\<close> function accordingly. Define two functions
    1.10 -\<open>pre_order\<close> and \<open>post_order\<close> of type \<open>'a tree2 \<Rightarrow> 'a list\<close>
    1.11 +Define the two functions
    1.12 +\<open>pre_order\<close> and \<open>post_order\<close> of type @{typ "'a tree \<Rightarrow> 'a list"}
    1.13  that traverse a tree and collect all stored values in the respective order in
    1.14  a list. Prove \<^prop>\<open>pre_order (mirror t) = rev (post_order t)\<close>.
    1.15  \end{exercise}