equal
deleted
inserted
replaced
127 apply(simp only: alpha_bi) |
127 apply(simp only: alpha_bi) |
128 apply(simp only: alpha_gen) |
128 apply(simp only: alpha_gen) |
129 apply(simp only: alpha_tst) |
129 apply(simp only: alpha_tst) |
130 apply(simp only: supp_eqvt[symmetric]) |
130 apply(simp only: supp_eqvt[symmetric]) |
131 apply(simp only: eqvts) |
131 apply(simp only: eqvts) |
132 defer (* hacking *) |
132 apply simp |
133 apply(simp add: supp_Abs_tst) |
133 apply(simp add: supp_Abs_tst) |
134 apply(simp add: fv_bi) |
134 apply(simp add: fv_bi) |
135 apply(rule Collect_cong) |
|
136 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
137 apply(simp) |
|
138 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
139 apply(simp) |
|
140 apply(rule Collect_cong) |
|
141 apply(blast) |
|
142 done |
135 done |
143 |
136 |
144 text {* example 2 *} |
137 text {* example 2 *} |
145 |
138 |
146 nominal_datatype trm' = |
139 nominal_datatype trm' = |