src/HOL/Finite.ML
changeset 5477 41ab0f44dd8f
parent 5476 1c09934fe445
child 5516 d80e9aeb4a2b
equal deleted inserted replaced
5476:1c09934fe445 5477:41ab0f44dd8f
   325 by (Clarify_tac 1);
   325 by (Clarify_tac 1);
   326 by (case_tac "x:B" 1);
   326 by (case_tac "x:B" 1);
   327  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
   327  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
   328  by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
   328  by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
   329 by (fast_tac (claset() addss
   329 by (fast_tac (claset() addss
   330 	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
   330 	      (simpset() addsimps [subset_insert_iff, finite_subset]
       
   331 			 delsimps [insert_subset])) 1);
   331 qed_spec_mp "card_mono";
   332 qed_spec_mp "card_mono";
   332 
   333 
   333 
   334 
   334 Goal "[| finite A; finite B |] \
   335 Goal "[| finite A; finite B |] \
   335 \     ==> card A + card B = card (A Un B) + card (A Int B)";
   336 \     ==> card A + card B = card (A Un B) + card (A Int B)";