src/HOL/Int.thy
changeset 61609 77b453bd616f
parent 61552 980dd46a03fb
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Int.thy	Tue Nov 03 11:20:21 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Tue Nov 10 14:18:41 2015 +0000
     1.3 @@ -238,7 +238,7 @@
     1.4  lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
     1.5    by simp
     1.6  
     1.7 -lemma of_int_power:
     1.8 +lemma of_int_power [simp]:
     1.9    "of_int (z ^ n) = of_int z ^ n"
    1.10    by (induct n) simp_all
    1.11  
    1.12 @@ -470,7 +470,7 @@
    1.13  context ring_1
    1.14  begin
    1.15  
    1.16 -lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
    1.17 +lemma of_nat_nat [simp]: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
    1.18    by transfer (clarsimp simp add: of_nat_diff)
    1.19  
    1.20  end