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/Code_Numeral.thy
changeset 44821 a92f65e174cf
parent 39818 ff9e9d5ac171
child 45694 4a8743618257 
--- a/src/HOL/Code_Numeral.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Code_Numeral.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -274,7 +274,7 @@
   then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" 
     by simp
   then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" 
-    unfolding int_mult zadd_int [symmetric] by simp
+    unfolding of_nat_mult of_nat_add by simp
   then show ?thesis by (auto simp add: int_of_def mult_ac)
 qed
isabelle