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_Integer.thy
changeset 47217 501b9bbd0d6e
parent 47125 a3a64240cd98
child 48073 1b609a7837ef 
--- a/src/HOL/Library/Code_Integer.thy	Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Mar 30 11:16:35 2012 +0200
@@ -22,7 +22,7 @@
 proof -
   have "2 = nat 2" by simp
   show ?thesis
-    apply (subst nat_mult_2 [symmetric])
+    apply (subst mult_2 [symmetric])
     apply (auto simp add: Let_def divmod_int_mod_div not_le
      nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
     apply (unfold `2 = nat 2`)
isabelle