--- a/src/ZF/Arith.ML Wed Jul 15 12:02:19 1998 +0200
+++ b/src/ZF/Arith.ML Wed Jul 15 14:13:18 1998 +0200
@@ -354,7 +354,7 @@
(*Type checking depends upon termination!*)
Goalw [div_def]
- "!!m n. [| 0<n; m:nat; n:nat |] ==> m div n : nat";
+ "[| 0<n; m:nat; n:nat |] ==> m div n : nat";
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
qed "div_type";
@@ -573,7 +573,7 @@
(*Thanks to Sten Agerholm*)
Goal (* add_le_elim1 *)
- "!!m n k. [|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
+ "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
by (etac rev_mp 1);
by (eres_inst_tac [("n","n")] nat_induct 1);
by (Asm_simp_tac 1);