src/HOL/ex/set.ML
changeset 2911 8a680e310f04
parent 2031 03a843f0f447
child 2935 998cb95fdd43
     1.1 --- a/src/HOL/ex/set.ML	Fri Apr 04 16:16:35 1997 +0200
     1.2 +++ b/src/HOL/ex/set.ML	Fri Apr 04 16:27:39 1997 +0200
     1.3 @@ -43,11 +43,11 @@
     1.4  
     1.5  (*** The Schroder-Berstein Theorem ***)
     1.6  
     1.7 -val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";
     1.8 +val prems = goalw Lfp.thy [image_def] "inj(f) ==> inv(f)``(f``X) = X";
     1.9  by (cut_facts_tac prems 1);
    1.10  by (rtac equalityI 1);
    1.11 -by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
    1.12 -by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
    1.13 +by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
    1.14 +by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
    1.15  qed "inv_image_comp";
    1.16  
    1.17  goal Set.thy "!!f. f(a) ~: (f``X) ==> a~:X";
    1.18 @@ -116,7 +116,7 @@
    1.19  by (rtac exI 1);
    1.20  by (rtac bij_if_then_else 1);
    1.21  by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1,
    1.22 -           rtac (injg RS inj_onto_Inv) 1]);
    1.23 +           rtac (injg RS inj_onto_inv) 1]);
    1.24  by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
    1.25              etac imageE, etac ssubst, rtac rangeI]);
    1.26  by (EVERY1 [etac ssubst, stac double_complement,