src/HOL/equalities.ML
changeset 9312 a93a7b6bb654
parent 9206 eaaee6bd74ba
child 9338 fcf7f29a3447
equal deleted inserted replaced
9311:ab5b24cbaa16 9312:a93a7b6bb654
   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)";