--- a/src/HOL/Integ/IntDef.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy Tue Oct 19 18:18:45 2004 +0200
@@ -344,11 +344,11 @@
subsection{*Strict Monotonicity of Multiplication*}
text{*strict, in 1st argument; proof is by induction on k>0*}
-lemma zmult_zless_mono2_lemma [rule_format]:
- "i<j ==> 0<k --> int k * i < int k * j"
-apply (induct_tac "k", simp)
+lemma zmult_zless_mono2_lemma:
+ "i<j ==> 0<k ==> int k * i < int k * j"
+apply (induct "k", simp)
apply (simp add: int_Suc)
-apply (case_tac "n=0")
+apply (case_tac "k=0")
apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
done