equal
deleted
inserted
replaced
869 by blast |
869 by blast |
870 |
870 |
871 lemma singleton_conv2 [simp]: "{x. a = x} = {a}" |
871 lemma singleton_conv2 [simp]: "{x. a = x} = {a}" |
872 by blast |
872 by blast |
873 |
873 |
874 lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B" |
874 lemma diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B" |
875 by blast |
875 by blast |
876 |
876 |
877 lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)" |
877 lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)" |
878 by (blast elim: equalityE) |
878 by (blast elim: equalityE) |
879 |
879 |