| changeset 58310 | 91ea607a34d8 |
| parent 58249 | 180f1b3508ed |
| child 58889 | 5b7a9633cfa8 |
| 58309:a09ec6daaa19 | 58310:91ea607a34d8 |
|---|---|
7 |
7 |
8 header {* Binary trees *} |
8 header {* Binary trees *} |
9 |
9 |
10 theory BT imports Main begin |
10 theory BT imports Main begin |
11 |
11 |
12 datatype_new 'a bt = |
12 datatype 'a bt = |
13 Lf |
13 Lf |
14 | Br 'a "'a bt" "'a bt" |
14 | Br 'a "'a bt" "'a bt" |
15 |
15 |
16 primrec n_nodes :: "'a bt => nat" where |
16 primrec n_nodes :: "'a bt => nat" where |
17 "n_nodes Lf = 0" |
17 "n_nodes Lf = 0" |