src/HOL/Int.thy

   by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
 
 lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
   by simp
 
-lemma of_int_power:
+lemma of_int_power [simp]:
   "of_int (z ^ n) = of_int z ^ n"
   by (induct n) simp_all
 
 end
 

   by transfer (clarsimp simp add: less_diff_conv)
 
 context ring_1
 begin
 
-lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
+lemma of_nat_nat [simp]: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
   by transfer (clarsimp simp add: of_nat_diff)
 
 end
 
 lemma diff_nat_numeral [simp]: