# HG changeset patch
# User paulson
# Date 906122411 -7200
# Node ID da4d0444ea852e8897d085ab451377ce89185ee0
# Parent  a63e0c326e6ce00be3150534fbf93a49134dec50
new theorem less_Suc_eq_le

diff -r a63e0c326e6c -r da4d0444ea85 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Sep 18 14:39:51 1998 +0200
+++ b/src/HOL/Auth/Shared.ML	Fri Sep 18 14:40:11 1998 +0200
@@ -139,8 +139,8 @@
 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_refl3, le_add2, le_add1, 
-				     le_eq_less_Suc RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2,
+				      less_Suc_eq_le]) 1);
 qed "Nonce_supply2";
 
 Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
@@ -152,8 +152,8 @@
 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_refl3, le_add2, le_add1, 
-				     le_eq_less_Suc RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2,
+				      less_Suc_eq_le]) 1);
 qed "Nonce_supply3";
 
 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
diff -r a63e0c326e6c -r da4d0444ea85 src/HOL/Induct/FoldSet.ML
--- a/src/HOL/Induct/FoldSet.ML	Fri Sep 18 14:39:51 1998 +0200
+++ b/src/HOL/Induct/FoldSet.ML	Fri Sep 18 14:40:11 1998 +0200
@@ -66,7 +66,7 @@
 by (Clarify_tac 1);
 (*force simplification of "card A < card (insert ...)"*)
 by (etac rev_mp 1);
-by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
 by (rtac impI 1);
 (** LEVEL 10 **)
 by (rename_tac "Aa xa ya Ab xb yb" 1);
diff -r a63e0c326e6c -r da4d0444ea85 src/HOL/UNITY/Deadlock.ML
--- a/src/HOL/UNITY/Deadlock.ML	Fri Sep 18 14:39:51 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML	Fri Sep 18 14:40:11 1998 +0200
@@ -73,8 +73,7 @@
 
 Goal "(INT i:{i. i <= Suc n}. A i) = \
 \         A 0 Int (INT i:{i. i <= n}. -A i Un A(Suc i))";
-by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym, 
-				  INT_le_equals_Int]) 1);
+by (simp_tac (simpset() addsimps [less_Suc_eq_le, INT_le_equals_Int]) 1);
 qed "INT_le_Suc_equals_Int";
 
 
diff -r a63e0c326e6c -r da4d0444ea85 src/HOL/ex/Recdefs.thy
--- a/src/HOL/ex/Recdefs.thy	Fri Sep 18 14:39:51 1998 +0200
+++ b/src/HOL/ex/Recdefs.thy	Fri Sep 18 14:40:11 1998 +0200
@@ -31,7 +31,7 @@
 
 consts qsort   ::"('a => 'a => bool) * 'a list => 'a list"
 recdef qsort "measure (size o snd)"
-    simpset "simpset() addsimps [le_eq_less_Suc RS sym, length_filter]"
+    simpset "simpset() addsimps [less_Suc_eq_le, length_filter]"
     "qsort(ord, [])    = []"
     "qsort(ord, x#rst) = qsort(ord, filter(Not o ord x) rst)  
                          @ [x] @   
@@ -44,7 +44,7 @@
 
 consts gcd :: "nat * nat => nat"
 recdef gcd "measure (%(x,y).x+y)"
-    simpset "simpset() addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
+    simpset "simpset() addsimps [less_Suc_eq_le, le_add1, diff_le_self]"
     "gcd (0,y)          = y"
     "gcd (Suc x, 0)     = Suc x"
     "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)