src/ZF/Finite.ML

 (*Every subset of a finite set is finite.*)
 goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
 by (etac Fin_induct 1);
 by (simp_tac (simpset() addsimps [subset_empty_iff]) 1);
 by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
 by (Asm_simp_tac 1);
 qed "Fin_subset_lemma";
 
 goal Finite.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";

 (*Every subset of a finite function is a finite function.*)
 goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
 by (etac FiniteFun.induct 1);
 by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1);
 by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
 by (dtac (spec RS mp) 1 THEN assume_tac 1);
 by (fast_tac (claset() addSIs FiniteFun.intrs) 1);
 qed "FiniteFun_subset_lemma";