1.1 --- a/src/HOL/Fun.ML	Wed Jul 15 14:13:18 1998 +0200
     1.2 +++ b/src/HOL/Fun.ML	Wed Jul 15 14:19:02 1998 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4  qed "inj_on_contraD";
     1.5  
     1.6  Goalw [inj_on_def]
     1.7 -    "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
     1.8 +    "[| A<=B; inj_on f B |] ==> inj_on f A";
     1.9  by (Blast_tac 1);
    1.10  qed "subset_inj_on";
    1.11  
    1.12 @@ -117,7 +117,7 @@
    1.13  (*** Lemmas about inj ***)
    1.14  
    1.15  Goalw [o_def]
    1.16 -    "!!f g. [| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
    1.17 +    "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
    1.18  by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
    1.19  qed "comp_inj";
    1.20  
    1.21 @@ -141,12 +141,12 @@
    1.22  qed "inj_on_inv";
    1.23  
    1.24  Goalw [inj_on_def]
    1.25 -   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
    1.26 +   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
    1.27  by (Blast_tac 1);
    1.28  qed "inj_on_image_Int";
    1.29  
    1.30  Goalw [inj_on_def]
    1.31 -   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
    1.32 +   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
    1.33  by (Blast_tac 1);
    1.34  qed "inj_on_image_set_diff";
    1.35