| changeset 58249 | 180f1b3508ed |
| parent 57512 | cc97b347b301 |
| child 58310 | 91ea607a34d8 |
| 58248:25af24e1f37b | 58249:180f1b3508ed |
|---|---|
11 imports Main |
11 imports Main |
12 begin |
12 begin |
13 |
13 |
14 declare [[metis_new_skolem]] |
14 declare [[metis_new_skolem]] |
15 |
15 |
16 datatype 'a bt = |
16 datatype_new 'a bt = |
17 Lf |
17 Lf |
18 | Br 'a "'a bt" "'a bt" |
18 | Br 'a "'a bt" "'a bt" |
19 |
19 |
20 primrec n_nodes :: "'a bt => nat" where |
20 primrec n_nodes :: "'a bt => nat" where |
21 "n_nodes Lf = 0" |
21 "n_nodes Lf = 0" |