equal
deleted
inserted
replaced
590 by (Blast_tac 1); |
590 by (Blast_tac 1); |
591 qed "INT_eq"; |
591 qed "INT_eq"; |
592 |
592 |
593 Goal "(UNION A B = {}) = (ALL x:A. B x = {})"; |
593 Goal "(UNION A B = {}) = (ALL x:A. B x = {})"; |
594 by Auto_tac; |
594 by Auto_tac; |
595 qed "UN_empty"; |
595 qed "UN_empty3"; |
596 AddIffs [UN_empty]; |
596 AddIffs [UN_empty3]; |
597 |
597 |
598 |
598 |
599 (*Distributive laws...*) |
599 (*Distributive laws...*) |
600 |
600 |
601 Goal "A Int Union(B) = (UN C:B. A Int C)"; |
601 Goal "A Int Union(B) = (UN C:B. A Int C)"; |