| changeset 935 | a94ef3eed456 |
| parent 753 | ec86863e87c8 |
| child 1171 | e4d6b42be73a |
| 934:2e0203309287 | 935:a94ef3eed456 |
|---|---|
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 Binary trees |
6 Binary trees |
7 *) |
7 *) |
8 |
8 |
9 BT = Univ + |
9 BT = Datatype + |
10 consts |
10 consts |
11 bt_rec :: "[i, i, [i,i,i,i,i]=>i] => i" |
11 bt_rec :: "[i, i, [i,i,i,i,i]=>i] => i" |
12 n_nodes :: "i=>i" |
12 n_nodes :: "i=>i" |
13 n_leaves :: "i=>i" |
13 n_leaves :: "i=>i" |
14 bt_reflect :: "i=>i" |
14 bt_reflect :: "i=>i" |