diff -r adcaaf6c9910 -r ff20b44b2fc8 src/HOL/Library/Tree.thy --- a/src/HOL/Library/Tree.thy Wed Jan 13 00:12:43 2016 +0100 +++ b/src/HOL/Library/Tree.thy Wed Jan 13 09:38:16 2016 +0100 @@ -7,8 +7,8 @@ begin datatype 'a tree = - Leaf ("\\") | - Node (left: "'a tree") (val: 'a) (right: "'a tree") ("\_, _, _\") + is_Leaf: Leaf ("\\") | + Node (left: "'a tree") (val: 'a) (right: "'a tree") ("(1\_,/ _,/ _\)") where "left Leaf = Leaf" | "right Leaf = Leaf"