Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Code_Target_Nat.thy
changeset 66190 a41435469559
parent 64997 067a6cca39f0
child 66808 1907167b6038 
--- a/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:33 2017 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:35 2017 +0200
@@ -59,7 +59,7 @@
 
 lemma [code abstract]:
   "integer_of_nat (nat_of_num n) = integer_of_num n"
-  by transfer (simp add: nat_of_num_numeral)
+  by (simp add: nat_of_num_numeral integer_of_nat_numeral)
 
 lemma [code abstract]:
   "integer_of_nat 0 = 0"
isabelle