| changeset 10212 | 33fe2d701ddd |
| parent 10045 | c76b73e16711 |
| child 10214 | 77349ed89f45 |
--- a/src/HOL/Real/Hyperreal/Series.ML Thu Oct 12 18:09:06 2000 +0200 +++ b/src/HOL/Real/Hyperreal/Series.ML Thu Oct 12 18:38:23 2000 +0200 @@ -94,9 +94,9 @@ [real_minus_add_distrib])); qed "sumr_minus"; -context Arith.thy; +context Arithmetic.thy; -goal Arith.thy "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m"; +Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m"; by (auto_tac (claset() addSDs [not_leE],simpset())); qed "lemma_not_Suc_add";