equal
deleted
inserted
replaced
622 qed "subset_iff"; |
622 qed "subset_iff"; |
623 |
623 |
624 goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))"; |
624 goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))"; |
625 by (Blast_tac 1); |
625 by (Blast_tac 1); |
626 qed "subset_iff_psubset_eq"; |
626 qed "subset_iff_psubset_eq"; |
|
627 |
|
628 goal Set.thy "(!x. x ~: A) = (A={})"; |
|
629 by(Blast_tac 1); |
|
630 qed "all_not_in_conv"; |
|
631 (* FIXME: AddIffs [all_not_in_conv]; *) |
627 |
632 |
628 goalw Set.thy [Pow_def] "Pow {} = {{}}"; |
633 goalw Set.thy [Pow_def] "Pow {} = {{}}"; |
629 by (Auto_tac()); |
634 by (Auto_tac()); |
630 qed "Pow_empty"; |
635 qed "Pow_empty"; |
631 Addsimps [Pow_empty]; |
636 Addsimps [Pow_empty]; |