changeset 62348 | 9a5f43dac883 |
parent 61649 | 268d88ec9087 |
child 63648 | f9f3006a5579 |
--- a/src/HOL/Nat_Transfer.thy Wed Feb 17 21:51:57 2016 +0100 +++ b/src/HOL/Nat_Transfer.thy Wed Feb 17 21:51:57 2016 +0100 @@ -286,7 +286,7 @@ "(int x) * (int y) = int (x * y)" "tsub (int x) (int y) = int (x - y)" "(int x)^n = int (x^n)" - by (auto simp add: int_mult tsub_def of_nat_power) + by (auto simp add: of_nat_mult tsub_def of_nat_power) lemma transfer_int_nat_function_closures: "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"