# HG changeset patch
# User paulson
# Date 927277006 -7200
# Node ID 62d1e642da30e3ff683174f491c126e35cebbf3d
# Parent  63e53327f5e5e57c8d945bc69d4951daa88ed0f5
preferring generic rules to specific ones...

diff -r 63e53327f5e5 -r 62d1e642da30 src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Fri May 21 10:50:04 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Fri May 21 10:56:46 1999 +0200
@@ -27,7 +27,7 @@
 by (rtac (constrains_imp_Constrains RS StableI) 1);
 by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
 by (constrains_tac 2);
-by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
+by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
 by (constrains_tac 1);
 qed "invFG";
 
diff -r 63e53327f5e5 -r 62d1e642da30 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Fri May 21 10:50:04 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML	Fri May 21 10:56:46 1999 +0200
@@ -155,11 +155,13 @@
 
 AddIffs [Min_le_n, n_le_Max];
 
-val le_MinD = Min_le_n RS zle_anti_sym;
-val Max_leD = n_le_Max RSN (2,zle_anti_sym);
+val le_MinD = Min_le_n RS order_antisym;
+val Max_leD = n_le_Max RSN (2,order_antisym);
 
-AddSDs [le_MinD, zleI RS le_MinD,
-	Max_leD, zleI RS Max_leD];
+val linorder_leI = linorder_not_less RS iffD1;
+
+AddSDs [le_MinD, linorder_leI RS le_MinD,
+	Max_leD, linorder_leI RS Max_leD];
 
 (*lem_lift_2_0 
   NOT an ensures property, but a mere inclusion;
@@ -194,7 +196,7 @@
 by (ensures_tac "move_up" 1);
 by Safe_tac;
 (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
-by (etac (zleI RS zle_anti_sym RS sym) 1);
+by (etac (linorder_leI RS order_antisym RS sym) 1);
 by (REPEAT_FIRST (eresolve_tac mov_metrics));
 by (REPEAT_FIRST distinct_tac);
 (** LEVEL 6 **)
@@ -213,7 +215,7 @@
 by (ensures_tac "move_down" 1);
 by Safe_tac;
 (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
-by (etac (zleI RS zle_anti_sym RS sym) 1);
+by (etac (linorder_leI RS order_antisym RS sym) 1);
 by (REPEAT_FIRST (eresolve_tac mov_metrics));
 by (REPEAT_FIRST distinct_tac);
 (** LEVEL 6 **)
@@ -354,7 +356,7 @@
 by (case_tac "#0 < z" 1);
 (*If z <= #0 then actually z = #0*)
 by (fold_tac [zle_def]);
-by (force_tac (claset() addIs [R_thm11, zle_anti_sym], simpset()) 2);
+by (force_tac (claset() addIs [R_thm11, order_antisym], simpset()) 2);
 by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
 by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
 by (rtac lift_3_Req 3);
diff -r 63e53327f5e5 -r 62d1e642da30 src/HOL/UNITY/Network.ML
--- a/src/HOL/UNITY/Network.ML	Fri May 21 10:50:04 1999 +0200
+++ b/src/HOL/UNITY/Network.ML	Fri May 21 10:56:46 1999 +0200
@@ -49,8 +49,8 @@
 by (Clarify_tac 1);
 by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
 		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
-by (REPEAT (blast_tac (claset() addIs [le_anti_sym, le_trans, eq_imp_le]) 2));
-
+by (REPEAT 
+    (blast_tac (claset() addIs [order_antisym, le_trans, eq_imp_le]) 2));
 by (Asm_simp_tac 1);
 result();
 
diff -r 63e53327f5e5 -r 62d1e642da30 src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Fri May 21 10:50:04 1999 +0200
+++ b/src/HOL/UNITY/Reach.ML	Fri May 21 10:56:46 1999 +0200
@@ -116,7 +116,7 @@
 by (ensures_tac "asgt a b" 1);
 by (Blast_tac 2);
 by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
-by (dtac (metric_le RS le_anti_sym) 1);
+by (dtac (metric_le RS order_antisym) 1);
 by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)],
 	      simpset()));
 qed "LeadsTo_Diff_fixedpoint";
diff -r 63e53327f5e5 -r 62d1e642da30 src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Fri May 21 10:50:04 1999 +0200
+++ b/src/HOL/ex/Puzzle.ML	Fri May 21 10:56:46 1999 +0200
@@ -55,7 +55,7 @@
 qed "f_mono";
 
 Goal "f(n) = n";
-by (rtac le_anti_sym 1);
+by (rtac order_antisym 1);
 by (rtac lemma1 2);
 by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1);
 result();