# HG changeset patch
# User paulson
# Date 882873647 -3600
# Node ID d17524e0beb0668cb2e1259b5c477d963fcab246
# Parent  bd05e2a28602a843c7e567da2cdcfbb5eb63a7ef
tidied

diff -r bd05e2a28602 -r d17524e0beb0 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue Dec 23 11:40:18 1997 +0100
+++ b/src/HOL/NatDef.ML	Tue Dec 23 11:40:47 1997 +0100
@@ -541,27 +541,25 @@
 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
 qed "le_refl";
 
-val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
-by (dtac le_imp_less_or_eq 1);
-by (blast_tac (claset() addIs [less_trans]) 1);
+goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
+by (blast_tac (claset() addSDs [le_imp_less_or_eq]
+	                addIs [less_trans]) 1);
 qed "le_less_trans";
 
 goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
-by (dtac le_imp_less_or_eq 1);
-by (blast_tac (claset() addIs [less_trans]) 1);
+by (blast_tac (claset() addSDs [le_imp_less_or_eq]
+	                addIs [less_trans]) 1);
 qed "less_le_trans";
 
 goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
-by (EVERY1[dtac le_imp_less_or_eq, 
-           dtac le_imp_less_or_eq,
-           rtac less_or_eq_imp_le, 
-           blast_tac (claset() addIs [less_trans])]);
+by (blast_tac (claset() addSDs [le_imp_less_or_eq]
+	                addIs [less_or_eq_imp_le, less_trans]) 1);
 qed "le_trans";
 
 goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
-by (EVERY1[dtac le_imp_less_or_eq, 
-           dtac le_imp_less_or_eq,
-           blast_tac (claset() addEs [less_irrefl,less_asym])]);
+(*order_less_irrefl could make this proof fail*)
+by (blast_tac (claset() addSDs [le_imp_less_or_eq]
+	                addSEs [less_irrefl] addEs [less_asym]) 1);
 qed "le_anti_sym";
 
 goal thy "(Suc(n) <= Suc(m)) = (n <= m)";