# HG changeset patch
# User paulson
# Date 976618724 -3600
# Node ID 37b9897dbf3a2fd261cf04a367eba2c5f69b7188
# Parent  175ccbd5415a9afa3389db406ff2af2b273edbfe
greater use of overloaded rules (order_less_imp_le not zless_imp_zle, ...)

diff -r 175ccbd5415a -r 37b9897dbf3a src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Tue Dec 12 11:57:33 2000 +0100
+++ b/src/HOL/Integ/Int.ML	Tue Dec 12 11:58:44 2000 +0100
@@ -107,7 +107,7 @@
 Goal "(w + int (Suc m) <= z) = (w + int m < z)";
 by (simp_tac (simpset() addsimps [zle_def, zless_add_int_Suc_eq]) 1);
 by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym],
-	      simpset() addsimps [zless_imp_zle, symmetric zle_def]));
+	      simpset() addsimps [order_less_imp_le, symmetric zle_def]));
 qed "add_int_Suc_zle_eq";
 
 
@@ -151,7 +151,7 @@
 qed "zadd_zle_mono";
 
 Goal "[| w'<w; z'<=z |] ==> w' + z' < w + (z::int)";
-by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
+by (etac (zadd_zless_mono1 RS order_less_le_trans) 1);
 by (Simp_tac 1);
 qed "zadd_zless_mono";
 
@@ -199,7 +199,7 @@
 qed "negative_zless_0"; 
 
 Goal "- (int (Suc n)) < int m";
-by (rtac (negative_zless_0 RS zless_zle_trans) 1);
+by (rtac (negative_zless_0 RS order_less_le_trans) 1);
 by (Simp_tac 1); 
 qed "negative_zless"; 
 AddIffs [negative_zless]; 
@@ -444,7 +444,7 @@
 				  inst "y1" "m*k" (linorder_not_le RS sym),
                                   inst "y1" "m" (linorder_not_le RS sym)]));
 by (ALLGOALS (etac notE));
-by (auto_tac (claset(), simpset() addsimps [zless_imp_zle, zmult_zle_mono1,
+by (auto_tac (claset(), simpset() addsimps [order_less_imp_le, zmult_zle_mono1,
                                             zmult_zle_mono1_neg]));  
 qed "zmult_zless_cancel2";
 
diff -r 175ccbd5415a -r 37b9897dbf3a src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Tue Dec 12 11:57:33 2000 +0100
+++ b/src/HOL/Integ/IntArith.ML	Tue Dec 12 11:58:44 2000 +0100
@@ -133,7 +133,7 @@
 qed "zmult_eq_self_iff";
 
 Goal "[| #1 < m; #1 < n |] ==> #1 < m*(n::int)";
-by (res_inst_tac [("z2.0","#1*n")] zless_trans 1);
+by (res_inst_tac [("y","#1*n")] order_less_trans 1);
 by (rtac zmult_zless_mono1 2);
 by (ALLGOALS Asm_simp_tac);
 qed "zless_1_zmult";