| changeset 9442 | 6f089616ae1f |
| parent 8177 | e59e93ad85eb |
| child 10962 | cda180b1e2e0 |
--- a/src/HOL/IMPP/Natural.ML Tue Jul 25 00:13:49 2000 +0200 +++ b/src/HOL/IMPP/Natural.ML Tue Jul 25 01:27:36 2000 +0200 @@ -38,7 +38,7 @@ goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)"; by (induct_tac "m'" 1); -by Auto_tac; +by (CLASIMPSET auto_tac); qed_spec_mp "Suc_le_D"; Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";