| changeset 1959 | 58f8379eca73 |
| parent 1662 | a6b55b9d2f22 |
| child 2469 | b50b8c0eec01 |
--- 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";