src/HOL/Finite.ML
changeset 5476 1c09934fe445
parent 5416 9f029e382b5d
child 5477 41ab0f44dd8f
equal deleted inserted replaced
5475:410172655d64 5476:1c09934fe445
   323 by (etac finite_induct 1);
   323 by (etac finite_induct 1);
   324 by (Simp_tac 1);
   324 by (Simp_tac 1);
   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])) 1);
   331 qed_spec_mp "card_mono";
   331 qed_spec_mp "card_mono";
   332 
   332 
   333 
   333