equal
deleted
inserted
replaced
73 apply (simp add: alphas trm_lts.eq_iff supp_at_base) |
73 apply (simp add: alphas trm_lts.eq_iff supp_at_base) |
74 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
74 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
75 apply (simp add: atom_eqvt fresh_star_def) |
75 apply (simp add: atom_eqvt fresh_star_def) |
76 done |
76 done |
77 |
77 |
|
78 (* |
|
79 declare permute_trm_raw_permute_lts_raw.simps[eqvt] |
|
80 declare alpha_gen_eqvt[eqvt] |
|
81 equivariance alpha_trm_raw |
|
82 *) |
|
83 |
78 end |
84 end |
79 |
85 |
80 |
86 |
81 |
87 |