| changeset 69655 | 2b56cbb02e8a |
| parent 69593 | 3dda49e08b9d |
| child 72313 | babd74b71ea8 |
--- a/src/HOL/Library/Tree.thy Mon Jan 14 14:46:12 2019 +0100 +++ b/src/HOL/Library/Tree.thy Mon Jan 14 16:10:56 2019 +0100 @@ -9,7 +9,7 @@ datatype 'a tree = Leaf ("\<langle>\<rangle>") | - Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)") + Node "'a tree" ("value": 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)") datatype_compat tree primrec left :: "'a tree \<Rightarrow> 'a tree" where