equal
deleted
inserted
replaced
596 goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))"; |
596 goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))"; |
597 by (Blast_tac 1); |
597 by (Blast_tac 1); |
598 qed "subset_iff_psubset_eq"; |
598 qed "subset_iff_psubset_eq"; |
599 |
599 |
600 goal thy "(!x. x ~: A) = (A={})"; |
600 goal thy "(!x. x ~: A) = (A={})"; |
601 by(Blast_tac 1); |
601 by (Blast_tac 1); |
602 qed "all_not_in_conv"; |
602 qed "all_not_in_conv"; |
603 AddIffs [all_not_in_conv]; |
603 AddIffs [all_not_in_conv]; |
604 |
604 |
605 goalw thy [Pow_def] "Pow {} = {{}}"; |
605 goalw thy [Pow_def] "Pow {} = {{}}"; |
606 by (Auto_tac()); |
606 by (Auto_tac()); |