| changeset 2120 | 2786ff1df475 |
| parent 2105 | e25b0fff0dd2 |
| 2119:238062c4c9f2 | 2120:2786ff1df475 |
|---|---|
30 thm trm_lts.induct |
30 thm trm_lts.induct |
31 thm trm_lts.distinct |
31 thm trm_lts.distinct |
32 thm trm_lts.supp |
32 thm trm_lts.supp |
33 thm trm_lts.fv[simplified trm_lts.supp] |
33 thm trm_lts.fv[simplified trm_lts.supp] |
34 |
34 |
35 equivariance alpha_trm_raw |
|
36 |
35 |
37 (* why is this not in HOL simpset? *) |
36 (* why is this not in HOL simpset? *) |
38 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
37 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
39 by auto |
38 by auto |
40 |
39 |