| changeset 69219 | d4cec24a1d87 |
| parent 69218 | 59aefb3b9e95 |
| child 69593 | 3dda49e08b9d |
--- a/src/HOL/Library/Tree.thy Thu Nov 01 11:26:38 2018 +0100 +++ b/src/HOL/Library/Tree.thy Thu Nov 01 12:23:54 2018 +0100 @@ -9,7 +9,7 @@ datatype 'a tree = Leaf ("\<langle>\<rangle>") | - Node "'a tree" (root: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)") + Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)") datatype_compat tree primrec left :: "'a tree \<Rightarrow> 'a tree" where