1.1 --- a/src/HOL/Finite.ML	Mon Jan 24 14:48:11 2000 +0100
     1.2 +++ b/src/HOL/Finite.ML	Tue Jan 25 09:25:43 2000 +0100
     1.3 @@ -797,14 +797,14 @@
     1.4  by (auto_tac (claset() addIs [finite_subset], simpset()));
     1.5  qed "choose_deconstruct";
     1.6  
     1.7 -Goal "[| finite(A); finite(B);  f : A funcset B;  inj_on f A |] \
     1.8 +Goal "[| finite(A); finite(B);  f``A <= B;  inj_on f A |] \
     1.9  \     ==> card A <= card B";
    1.10  by (auto_tac (claset() addIs [card_mono], 
    1.11 -	      simpset() addsimps [card_image RS sym, Pi_def]));
    1.12 +	      simpset() addsimps [card_image RS sym]));
    1.13  qed "card_inj_on_le";
    1.14  
    1.15  Goal "[| finite A; finite B; \
    1.16 -\        f: A funcset B; inj_on f A; g: B funcset A; inj_on g B |] \
    1.17 +\        f``A <= B; inj_on f A; g``B <= A; inj_on g B |] \
    1.18  \     ==> card(A) = card(B)";
    1.19  by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset()));
    1.20  qed "card_bij_eq";
    1.21 @@ -812,17 +812,12 @@
    1.22  Goal "[| finite M; x ~: M |]  \
    1.23  \     ==> card{s. EX t. t <= M & card(t) = k & s = insert x t} = \
    1.24  \         card {s. s <= M & card(s) = k}";
    1.25 -by (res_inst_tac
    1.26 -    [("f", "lam s: {s. EX t. t <= M & card t = k & s = insert x t}. s - {x}"),
    1.27 -     ("g","lam s: {s. s <= M & card s = k}. insert x s")] card_bij_eq 1);
    1.28 +by (res_inst_tac [("f", "%s. s - {x}"), ("g","insert x")] card_bij_eq 1);
    1.29  by (res_inst_tac [("B","Pow(insert x M)")] finite_subset 1);
    1.30  by (res_inst_tac [("B","Pow(M)")] finite_subset 3);
    1.31 -by (TRYALL (Fast_tac));
    1.32 -by (rtac funcsetI 3);
    1.33 -by (rtac funcsetI 1);
    1.34 +by(REPEAT(Fast_tac 1));
    1.35  (* arity *)
    1.36 -by (auto_tac (claset() addSEs [equalityE], 
    1.37 -	      simpset() addsimps [inj_on_def, restrict_def]));
    1.38 +by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def]));
    1.39  by (stac Diff_insert0 1);
    1.40  by Auto_tac;
    1.41  qed "constr_bij";