equal
deleted
inserted
replaced
27 thm trm_lts.perm |
27 thm trm_lts.perm |
28 thm trm_lts.induct |
28 thm trm_lts.induct |
29 thm trm_lts.distinct |
29 thm trm_lts.distinct |
30 thm trm_lts.supp |
30 thm trm_lts.supp |
31 thm trm_lts.fv[simplified trm_lts.supp] |
31 thm trm_lts.fv[simplified trm_lts.supp] |
|
32 |
|
33 declare permute_trm_raw_permute_lts_raw.simps[eqvt] |
|
34 declare alpha_gen_eqvt[eqvt] |
|
35 |
|
36 equivariance alpha_trm_raw |
32 |
37 |
33 (* why is this not in HOL simpset? *) |
38 (* why is this not in HOL simpset? *) |
34 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
39 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
35 by auto |
40 by auto |
36 |
41 |