| changeset 2438 | abafea9b39bb |
| parent 2436 | 3885dc2669f9 |
| child 2449 | 6b51117b8955 |
| 2436:3885dc2669f9 | 2438:abafea9b39bb |
|---|---|
18 bn |
18 bn |
19 where |
19 where |
20 "bn Lnil = []" |
20 "bn Lnil = []" |
21 | "bn (Lcons x t l) = (atom x) # (bn l)" |
21 | "bn (Lcons x t l) = (atom x) # (bn l)" |
22 |
22 |
23 text {* *} |
|
23 |
24 |
24 (* |
25 (* |
25 |
26 |
26 thm trm_lts.fv |
27 thm trm_lts.fv |
27 thm trm_lts.eq_iff |
28 thm trm_lts.eq_iff |