src/HOL/Nat.ML
changeset 1024 b86042000035
parent 972 e61b058d58d2
child 1264 3eb91524b938
     1.1 --- a/src/HOL/Nat.ML	Mon Apr 10 08:13:13 1995 +0200
     1.2 +++ b/src/HOL/Nat.ML	Mon Apr 10 08:40:58 1995 +0200
     1.3 @@ -240,8 +240,9 @@
     1.4      "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
     1.5  \    |] ==> P";
     1.6  by (rtac (major RS tranclE) 1);
     1.7 -by (fast_tac (HOL_cs addSEs (prems@[pred_natE, Pair_inject])) 1);
     1.8 -by (fast_tac (HOL_cs addSEs (prems@[pred_natE, Pair_inject])) 1);
     1.9 +by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE'
    1.10 +		  eresolve_tac (prems@[pred_natE, Pair_inject])));
    1.11 +by (rtac refl 1);
    1.12  qed "lessE";
    1.13  
    1.14  goal Nat.thy "~ n<0";