diff -r b594e9277be3 -r 1335462046e8 src/HOL/Data_Structures/Tree23.thy --- 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 \ nat" datatype 'a tree23 = - Leaf | - Node2 "'a tree23" 'a "'a tree23" | - Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23" + Leaf ("\\") | + Node2 "'a tree23" 'a "'a tree23" ("\_, _, _\") | + Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23" ("\_, _, _, _, _\") fun inorder :: "'a tree23 \ 'a list" where "inorder Leaf = []" |