equal
deleted
inserted
replaced
29 thm trm_lts.perm |
29 thm trm_lts.perm |
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 |
|
35 declare permute_trm_raw_permute_lts_raw.simps[eqvt] |
|
36 |
34 |
37 equivariance alpha_trm_raw |
35 equivariance alpha_trm_raw |
38 |
36 |
39 (* why is this not in HOL simpset? *) |
37 (* why is this not in HOL simpset? *) |
40 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
38 lemma set_sub: "{a, b} - {b} = {a} - {b}" |