changeset 15251 | bb6f072c8d10 |
parent 15234 | ec91a90c604e |
child 15531 | 08c8dad8e399 |
--- a/src/HOL/Hyperreal/NSA.thy Mon Oct 18 13:40:45 2004 +0200 +++ b/src/HOL/Hyperreal/NSA.thy Tue Oct 19 18:18:45 2004 +0200 @@ -1961,7 +1961,7 @@ hence cannot belong to FreeUltrafilterNat -------------------------------------------*) lemma finite_nat_segment: "finite {n::nat. n < m}" -apply (induct_tac "m") +apply (induct "m") apply (auto simp add: Suc_Un_eq) done