equal
deleted
inserted
replaced
638 then show "x \<in> A \<union> B" using pi |
638 then show "x \<in> A \<union> B" using pi |
639 apply (induct pi arbitrary: x B rule: rev_induct) |
639 apply (induct pi arbitrary: x B rule: rev_induct) |
640 apply simp |
640 apply simp |
641 apply (simp add: split_paired_all supp_eqvt) |
641 apply (simp add: split_paired_all supp_eqvt) |
642 apply (drule perm_mem_left) |
642 apply (drule perm_mem_left) |
643 apply (simp add: calc_atm split: split_if_asm) |
643 apply (simp add: calc_atm split: if_split_asm) |
644 apply (auto dest: perm_mem_right) |
644 apply (auto dest: perm_mem_right) |
645 done |
645 done |
646 qed |
646 qed |
647 |
647 |
648 lemma abs_pat_alpha': |
648 lemma abs_pat_alpha': |