src/HOL/NatDef.ML
changeset 3085 f45074fab9c7
parent 3040 7d48671753da
child 3143 d60e49b86c6a
     1.1 --- a/src/HOL/NatDef.ML	Wed Apr 30 13:38:38 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Wed Apr 30 13:39:56 1997 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4  bind_thm ("less_irrefl", (less_not_refl RS notE));
     1.5  
     1.6  goal thy "!!m. n<m ==> m ~= (n::nat)";
     1.7 -by (blast_tac (!claset addEs [less_irrefl]) 1);
     1.8 +by (blast_tac (!claset addSEs [less_irrefl]) 1);
     1.9  qed "less_not_refl2";
    1.10  
    1.11  
    1.12 @@ -468,7 +468,7 @@
    1.13  
    1.14  goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
    1.15  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.16 -by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
    1.17 +by (blast_tac (!claset addSEs [less_irrefl,less_asym]) 1);
    1.18  qed "lessD";
    1.19  
    1.20  goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
    1.21 @@ -505,8 +505,7 @@
    1.22  
    1.23  goalw thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
    1.24  by (cut_facts_tac [less_linear] 1);
    1.25 -by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
    1.26 -by (flexflex_tac);
    1.27 +by (blast_tac (!claset addSEs [less_irrefl] addEs [less_asym]) 1);
    1.28  qed "less_or_eq_imp_le";
    1.29  
    1.30  goal thy "(x <= (y::nat)) = (x < y | x=y)";