--- a/src/HOL/Hoare/Examples.ML Thu Oct 01 18:22:24 1998 +0200
+++ b/src/HOL/Hoare/Examples.ML Thu Oct 01 18:23:00 1998 +0200
@@ -40,7 +40,7 @@
by (etac gcd_nnn 4);
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
by (force_tac (claset(),
- simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2);
+ simpset() addsimps [not_less_iff_le, order_le_less]) 2);
by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
qed "Euclid_GCD";
--- a/src/HOL/NatDef.ML Thu Oct 01 18:22:24 1998 +0200
+++ b/src/HOL/NatDef.ML Thu Oct 01 18:23:00 1998 +0200
@@ -383,10 +383,6 @@
by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1);
qed "Suc_le_eq";
-(*For instance, (Suc m < Suc n) = (Suc m <= n) = (m<n) *)
-val le_simps = [less_Suc_eq_le, Suc_le_eq];
-
-
Goalw [le_def] "m <= n ==> m <= Suc n";
by (blast_tac (claset() addDs [Suc_lessD]) 1);
qed "le_SucI";
@@ -398,6 +394,9 @@
by (blast_tac (claset() addEs [less_asym]) 1);
qed "less_imp_le";
+(*For instance, (Suc m < Suc n) = (Suc m <= n) = (m<n) *)
+val le_simps = [less_imp_le, less_Suc_eq_le, Suc_le_eq];
+
(** Equivalence of m<=n and m<n | m=n **)
@@ -421,11 +420,8 @@
Goal "n <= (n::nat)";
by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
qed "le_refl";
-AddSIs [le_refl];
-(*Obvious ways of proving m<=n;
- adding these rules to claset might be risky*)
-Addsimps [le_refl, less_imp_le];
+AddIffs [le_refl];
Goal "[| i <= j; j < k |] ==> i < (k::nat)";
--- a/src/HOL/arith_data.ML Thu Oct 01 18:22:24 1998 +0200
+++ b/src/HOL/arith_data.ML Thu Oct 01 18:23:00 1998 +0200
@@ -230,5 +230,5 @@
by (Clarify_tac 2);
by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
- Suc_diff_le]) 1);
+ Suc_diff_le, less_imp_le]) 1);
qed_spec_mp "diff_less_mono2";