# HG changeset patch
# User paulson
# Date 907258980 -7200
# Node ID fbb4e1ac234d39a769cb51759983599d4215c5a2
# Parent  477fc12adceb4c55d875a9cfc3fa0df63ada8041
tidied

diff -r 477fc12adceb -r fbb4e1ac234d src/HOL/Hoare/Examples.ML
--- 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";
 
diff -r 477fc12adceb -r fbb4e1ac234d src/HOL/NatDef.ML
--- 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)";
diff -r 477fc12adceb -r fbb4e1ac234d src/HOL/arith_data.ML
--- 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";