| changeset 13187 | e5434b822a96 |
| parent 12486 | 0ed8bdd883e0 |
| child 14269 | 502a7c95de73 |
--- a/src/HOL/Hyperreal/MacLaurin.ML Thu May 30 10:12:11 2002 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.ML Thu May 30 10:12:52 2002 +0200 @@ -443,8 +443,6 @@ Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3"; by (case_tac "d" 1 THEN Auto_tac); -by (case_tac "nat" 1 THEN Auto_tac); -by (case_tac "nata" 1 THEN Auto_tac); qed "lemma_exhaust_less_4"; bind_thm ("real_mult_le_lemma",