equal
deleted
inserted
replaced
5 |
5 |
6 text {* example 3 or example 5 from Terms.thy *} |
6 text {* example 3 or example 5 from Terms.thy *} |
7 |
7 |
8 atom_decl name |
8 atom_decl name |
9 |
9 |
10 ML {* val _ = cheat_alpha_eqvt := true *} |
|
11 ML {* val _ = cheat_equivp := true *} |
10 ML {* val _ = cheat_equivp := true *} |
12 |
11 |
13 nominal_datatype trm = |
12 nominal_datatype trm = |
14 Vr "name" |
13 Vr "name" |
15 | Ap "trm" "trm" |
14 | Ap "trm" "trm" |
81 apply (simp add: alphas trm_lts.eq_iff supp_at_base) |
80 apply (simp add: alphas trm_lts.eq_iff supp_at_base) |
82 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
81 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
83 apply (simp add: atom_eqvt fresh_star_def) |
82 apply (simp add: atom_eqvt fresh_star_def) |
84 done |
83 done |
85 |
84 |
86 (* |
|
87 declare permute_trm_raw_permute_lts_raw.simps[eqvt] |
|
88 declare alpha_gen_eqvt[eqvt] |
|
89 equivariance alpha_trm_raw |
|
90 *) |
|
91 |
|
92 end |
85 end |
93 |
86 |
94 |
87 |
95 |
88 |