src/ZF/equalities.ML
changeset 9303 f1ad1ed0d110
parent 9180 3bda56c0d70d
child 9907 473a6604da94
equal deleted inserted replaced
9302:8adf653d40a1 9303:f1ad1ed0d110
   599 Addsimps [Pow_0, Union_Pow_eq, Pow_Int_eq];
   599 Addsimps [Pow_0, Union_Pow_eq, Pow_Int_eq];
   600 
   600 
   601 (** RepFun **)
   601 (** RepFun **)
   602 
   602 
   603 Goal "{f(x).x:A}=0 <-> A=0";
   603 Goal "{f(x).x:A}=0 <-> A=0";
   604 	(*blast_tac takes too long to find a good depth*)
   604 by (Blast_tac 1);
   605 by (Blast.depth_tac (claset() addSEs [equalityE]) 10 1);
       
   606 qed "RepFun_eq_0_iff";
   605 qed "RepFun_eq_0_iff";
   607 
   606 
   608 (** Collect **)
   607 (** Collect **)
   609 
   608 
   610 Goal "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
   609 Goal "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";