src/HOL/Integ/IntDiv.thy

   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
 
 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
-apply (induct_tac "y", auto)
+apply (induct "y", auto)
 apply (rule zmod_zmult1_eq [THEN trans])
 apply (simp (no_asm_simp))
 apply (rule zmod_zmult_distrib [symmetric])
 done
 

 lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
   by (rule Power.power_mult [symmetric])
 
 lemma zero_less_zpower_abs_iff [simp]:
      "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: zero_less_mult_iff)
 done
 
 lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: zero_le_mult_iff)
 done
 
 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)