# HG changeset patch
# User paulson
# Date 932978094 -7200
# Node ID 00a0c20c81aece08d0f619ea8de93b8edffbc0ad
# Parent  b551a5a8966c07bf62e2696699ee11fd889e4861
tidied

diff -r b551a5a8966c -r 00a0c20c81ae src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Fri Jul 23 17:49:35 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Mon Jul 26 10:34:54 1999 +0200
@@ -90,12 +90,12 @@
 (*"v<=w ==> z+v <= z+w"*)
 bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2);
 
-Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
+Goal "[| w'<=w; z'<=z |] ==> w' + z' <= w + (z::int)";
 by (etac (zadd_zle_mono1 RS zle_trans) 1);
 by (Simp_tac 1);
 qed "zadd_zle_mono";
 
-Goal "!!z z'::int. [| w'<w; z'<=z |] ==> w' + z' < w + z";
+Goal "[| w'<w; z'<=z |] ==> w' + z' < w + (z::int)";
 by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
 by (Simp_tac 1);
 qed "zadd_zless_mono";
@@ -220,7 +220,7 @@
 by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); 
 qed "not_neg_nat"; 
 
-Goal "neg x ==> ? n. x = - (int (Suc n))"; 
+Goal "neg x ==> EX n. x = - (int (Suc n))"; 
 by (auto_tac (claset(), 
 	      simpset() addsimps [neg_eq_less_int0, zless_iff_Suc_zadd,
 				  zdiff_eq_eq RS sym, zdiff_def])); 
@@ -255,7 +255,7 @@
 
 Goal "(0 < nat z) = (int 0 < z)";
 by (stac (order_refl RS nat_le_int0 RS sym) 1);
-by (stac (zless_nat_conj) 1);
+by (stac zless_nat_conj 1);
 by (Simp_tac 1);
 qed "zless_zero_nat";