--- 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";
--- 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);
--- 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";
--- 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)