src/HOL/equalities.ML
changeset 4615 67457d16cdbc
parent 4609 b435c5a320b0
child 4634 83d364462ce1
equal deleted inserted replaced
4614:122015efd4e1 4615:67457d16cdbc
   316 qed "Compl_UN";
   316 qed "Compl_UN";
   317 
   317 
   318 goal thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
   318 goal thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
   319 by (Blast_tac 1);
   319 by (Blast_tac 1);
   320 qed "Compl_INT";
   320 qed "Compl_INT";
       
   321 
       
   322 Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];
   321 
   323 
   322 (*Halmos, Naive Set Theory, page 16.*)
   324 (*Halmos, Naive Set Theory, page 16.*)
   323 
   325 
   324 goal thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
   326 goal thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
   325 by (blast_tac (claset() addSEs [equalityCE]) 1);
   327 by (blast_tac (claset() addSEs [equalityCE]) 1);