--- a/src/ZF/AC/DC_lemmas.ML Wed Jul 15 12:02:19 1998 +0200
+++ b/src/ZF/AC/DC_lemmas.ML Wed Jul 15 14:13:18 1998 +0200
@@ -26,7 +26,7 @@
qed "n_lesspoll_nat";
Goalw [lepoll_def]
- "!!f. [| f:X->Y; Ord(X) |] ==> f``X lepoll X";
+ "[| f:X->Y; Ord(X) |] ==> f``X lepoll X";
by (res_inst_tac [("x","lam x:f``X. LEAST y. f`y = x")] exI 1);
by (res_inst_tac [("d","%z. f`z")] lam_injective 1);
by (fast_tac (claset() addSIs [Least_in_Ord, apply_equality]) 1);
@@ -91,7 +91,7 @@
qed "succ_in_succ";
Goalw [restrict_def]
- "!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x";
+ "[| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x";
by (etac subst 1);
by (Asm_full_simp_tac 1);
qed "restrict_eq_imp_val_eq";