# HG changeset patch
# User paulson
# Date 862400396 -7200
# Node ID f45074fab9c7dc63b05366cb3d43fc4fb2364e8b
# Parent  9844abe1de72e74f6dc2aafe53cc4f4a1fbb841b
Fixed clasets so that blast_tac would work

diff -r 9844abe1de72 -r f45074fab9c7 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Apr 30 13:38:38 1997 +0200
+++ b/src/HOL/NatDef.ML	Wed Apr 30 13:39:56 1997 +0200
@@ -251,7 +251,7 @@
 bind_thm ("less_irrefl", (less_not_refl RS notE));
 
 goal thy "!!m. n<m ==> m ~= (n::nat)";
-by (blast_tac (!claset addEs [less_irrefl]) 1);
+by (blast_tac (!claset addSEs [less_irrefl]) 1);
 qed "less_not_refl2";
 
 
@@ -468,7 +468,7 @@
 
 goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
+by (blast_tac (!claset addSEs [less_irrefl,less_asym]) 1);
 qed "lessD";
 
 goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
@@ -505,8 +505,7 @@
 
 goalw thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
-by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
-by (flexflex_tac);
+by (blast_tac (!claset addSEs [less_irrefl] addEs [less_asym]) 1);
 qed "less_or_eq_imp_le";
 
 goal thy "(x <= (y::nat)) = (x < y | x=y)";