# HG changeset patch
# User paulson
# Date 903623132 -7200
# Node ID 6d6467c2b8b9667c28b7fd88c0facd743cf3d507
# Parent  165b9c212cafc9f310abfd8c51b0999ff1dea30e
tidied

diff -r 165b9c212caf -r 6d6467c2b8b9 src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Thu Aug 20 16:23:43 1998 +0200
+++ b/src/HOL/Auth/Recur.ML	Thu Aug 20 16:25:32 1998 +0200
@@ -39,8 +39,7 @@
           (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
           recur.RA4) 2);
 by basic_possibility_tac;
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, 
-			       less_not_refl2 RS not_sym] 1));
+by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1));
 result();
 
 
@@ -60,8 +59,7 @@
 by basic_possibility_tac;
 by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
 		 ORELSE
-		 eresolve_tac [asm_rl, less_not_refl2, 
-			       less_not_refl2 RS not_sym] 1));
+		 eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1));
 result();
 ****************)
 
diff -r 165b9c212caf -r 6d6467c2b8b9 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Thu Aug 20 16:23:43 1998 +0200
+++ b/src/HOL/Auth/Shared.ML	Thu Aug 20 16:25:32 1998 +0200
@@ -139,8 +139,7 @@
 by (Clarify_tac 1);
 by (res_inst_tac [("x","N")] exI 1);
 by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
-by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym, 
-				     le_add2, le_add1, 
+by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add2, le_add1, 
 				     le_eq_less_Suc RS sym]) 1);
 qed "Nonce_supply2";
 
@@ -153,8 +152,7 @@
 by (res_inst_tac [("x","N")] exI 1);
 by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
 by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
-by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym, 
-				     le_add2, le_add1, 
+by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add2, le_add1, 
 				     le_eq_less_Suc RS sym]) 1);
 qed "Nonce_supply3";
 
diff -r 165b9c212caf -r 6d6467c2b8b9 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Thu Aug 20 16:23:43 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Thu Aug 20 16:25:32 1998 +0200
@@ -57,8 +57,7 @@
 qed "subst_gt";
 
 Goal "j<i ==> (Var j)[u/i] = Var(j)";
-by (asm_full_simp_tac (addsplit(simpset()) addsimps
-                          [less_not_refl2 RS not_sym,less_SucI]) 1);
+by (asm_full_simp_tac (addsplit(simpset()) addsimps [less_not_refl3]) 1);
 qed "subst_lt";
 
 Addsimps [subst_eq,subst_gt,subst_lt];