equal
deleted
inserted
replaced
5 theory Tree |
5 theory Tree |
6 imports Main |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
9 datatype 'a tree = |
9 datatype 'a tree = |
10 Leaf ("\<langle>\<rangle>") | |
10 is_Leaf: Leaf ("\<langle>\<rangle>") | |
11 Node (left: "'a tree") (val: 'a) (right: "'a tree") ("\<langle>_, _, _\<rangle>") |
11 Node (left: "'a tree") (val: 'a) (right: "'a tree") ("(1\<langle>_,/ _,/ _\<rangle>)") |
12 where |
12 where |
13 "left Leaf = Leaf" |
13 "left Leaf = Leaf" |
14 | "right Leaf = Leaf" |
14 | "right Leaf = Leaf" |
15 datatype_compat tree |
15 datatype_compat tree |
16 |
16 |