equal
deleted
inserted
replaced
470 |
470 |
471 section "UN and INT"; |
471 section "UN and INT"; |
472 |
472 |
473 (*Basic identities*) |
473 (*Basic identities*) |
474 |
474 |
475 bind_thm ("not_empty", prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1])); |
475 bind_thm ("not_empty", prove_goal thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1])); |
476 |
476 |
477 Goal "(UN x:{}. B x) = {}"; |
477 Goal "(UN x:{}. B x) = {}"; |
478 by (Blast_tac 1); |
478 by (Blast_tac 1); |
479 qed "UN_empty"; |
479 qed "UN_empty"; |
480 Addsimps[UN_empty]; |
480 Addsimps[UN_empty]; |