--- a/src/HOL/Data_Structures/Tree23.thy Sun Nov 15 12:45:28 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23.thy Sun Nov 15 14:38:29 2015 +0100
@@ -10,9 +10,9 @@
fixes height :: "'a \<Rightarrow> nat"
datatype 'a tree23 =
- Leaf |
- Node2 "'a tree23" 'a "'a tree23" |
- Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23"
+ Leaf ("\<langle>\<rangle>") |
+ Node2 "'a tree23" 'a "'a tree23" ("\<langle>_, _, _\<rangle>") |
+ Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23" ("\<langle>_, _, _, _, _\<rangle>")
fun inorder :: "'a tree23 \<Rightarrow> 'a list" where
"inorder Leaf = []" |