src/HOL/Fun.ML
changeset 5148 74919e8f221c
parent 5143 b94cd208f073
child 5305 513925de8962
--- a/src/HOL/Fun.ML	Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Fun.ML	Wed Jul 15 14:19:02 1998 +0200
@@ -109,7 +109,7 @@
 qed "inj_on_contraD";
 
 Goalw [inj_on_def]
-    "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
+    "[| A<=B; inj_on f B |] ==> inj_on f A";
 by (Blast_tac 1);
 qed "subset_inj_on";
 
@@ -117,7 +117,7 @@
 (*** Lemmas about inj ***)
 
 Goalw [o_def]
-    "!!f g. [| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
+    "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
 by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
 qed "comp_inj";
 
@@ -141,12 +141,12 @@
 qed "inj_on_inv";
 
 Goalw [inj_on_def]
-   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
+   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
 by (Blast_tac 1);
 qed "inj_on_image_Int";
 
 Goalw [inj_on_def]
-   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
+   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
 by (Blast_tac 1);
 qed "inj_on_image_set_diff";