equal
deleted
inserted
replaced
230 apply(simp only: Un_left_commute) |
230 apply(simp only: Un_left_commute) |
231 apply(simp only: Un_assoc[symmetric]) |
231 apply(simp only: Un_assoc[symmetric]) |
232 apply(simp only: Un_commute) |
232 apply(simp only: Un_commute) |
233 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
233 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
234 apply(simp only: Collect_disj_eq[symmetric] inf_or) |
234 apply(simp only: Collect_disj_eq[symmetric] inf_or) |
|
235 apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric]) |
235 sorry |
236 sorry |
236 |
237 |
237 lemma supp_fv: |
238 lemma supp_fv: |
238 "supp t = fv_trm1 t" |
239 "supp t = fv_trm1 t" |
239 "supp b = fv_bp b" |
240 "supp b = fv_bp b" |