# HG changeset patch
# User lcp
# Date 797160073 -7200
# Node ID e65129244146f74e71b579bcb9eb97526af26672
# Parent  efd07203ceec8f6a25e87a516a1dda696d8f0a4e
Changed proof of lessE for new hyp_subst_tac

diff -r efd07203ceec -r e65129244146 Nat.ML
--- a/Nat.ML	Thu Apr 06 11:18:02 1995 +0200
+++ b/Nat.ML	Thu Apr 06 11:21:13 1995 +0200
@@ -240,8 +240,9 @@
     "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
 \    |] ==> P";
 by (rtac (major RS tranclE) 1);
-by (fast_tac (HOL_cs addSEs (prems@[pred_natE, Pair_inject])) 1);
-by (fast_tac (HOL_cs addSEs (prems@[pred_natE, Pair_inject])) 1);
+by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE'
+		  eresolve_tac (prems@[pred_natE, Pair_inject])));
+by (rtac refl 1);
 qed "lessE";
 
 goal Nat.thy "~ n<0";