| changeset 1653 | a2142526bb01 |
| parent 1651 | f731e9aff866 |
| child 1658 | aacab5f67333 |
| 1652:3b9c05d158f3 | 1653:a2142526bb01 |
|---|---|
19 binder |
19 binder |
20 bn |
20 bn |
21 where |
21 where |
22 "bn Lnil = {}" |
22 "bn Lnil = {}" |
23 | "bn (Lcons x t l) = {atom x} \<union> (bn l)" |
23 | "bn (Lcons x t l) = {atom x} \<union> (bn l)" |
24 |
|
25 |
|
26 |
24 |
27 thm trm_lts.fv |
25 thm trm_lts.fv |
28 thm trm_lts.eq_iff |
26 thm trm_lts.eq_iff |
29 thm trm_lts.bn |
27 thm trm_lts.bn |
30 thm trm_lts.perm |
28 thm trm_lts.perm |