equal
deleted
inserted
replaced
784 |
784 |
785 lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P" |
785 lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P" |
786 by simp |
786 by simp |
787 |
787 |
788 lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast |
788 lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast |
|
789 |
|
790 lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)" |
|
791 by blast |
789 |
792 |
790 |
793 |
791 subsubsection {* Augmenting a set -- insert *} |
794 subsubsection {* Augmenting a set -- insert *} |
792 |
795 |
793 lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)" |
796 lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)" |