src/HOL/Nat_Transfer.thy
changeset 66795 420d0080545f
parent 64272 f76b6dda2e56
child 66817 0b12755ccbb2
     1.1 --- a/src/HOL/Nat_Transfer.thy	Mon Oct 09 16:14:18 2017 +0100
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:19 2017 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4      "(int x) * (int y) = int (x * y)"
     1.5      "tsub (int x) (int y) = int (x - y)"
     1.6      "(int x)^n = int (x^n)"
     1.7 -  by (auto simp add: of_nat_mult tsub_def of_nat_power)
     1.8 +  by (auto simp add: tsub_def)
     1.9  
    1.10  lemma transfer_int_nat_function_closures:
    1.11      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"