# HG changeset patch
# User paulson
# Date 841999548 -7200
# Node ID 58f8379eca731c6e604e47fd68c13994285b8745
# Parent  6f20ecbd87cbbdb5f431fb54cf34c877d7f64764
Modified proof to work with miniscoping

diff -r 6f20ecbd87cb -r 58f8379eca73 src/FOL/ex/Nat2.ML
--- a/src/FOL/ex/Nat2.ML	Thu Sep 05 18:42:48 1996 +0200
+++ b/src/FOL/ex/Nat2.ML	Fri Sep 06 10:45:48 1996 +0200
@@ -134,6 +134,7 @@
 by (simp_tac nat_ss 1);
 by (resolve_tac [impI RS allI] 1);
 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+by (resolve_tac [impI] 1);
 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
 by (fast_tac FOL_cs 1);
 qed "le_trans";