--- 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();
****************)
--- 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";
--- 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];