| changeset 15251 | bb6f072c8d10 |
| parent 15140 | 322485b816ac |
| child 19765 | dfe940911617 |
--- a/src/HOL/Hyperreal/EvenOdd.thy Mon Oct 18 13:40:45 2004 +0200 +++ b/src/HOL/Hyperreal/EvenOdd.thy Tue Oct 19 18:18:45 2004 +0200 @@ -13,7 +13,7 @@ subsection{*General Lemmas About Division*} lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" -apply (induct_tac "m") +apply (induct "m") apply (simp_all add: mod_Suc) done