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/Word/Misc_Numeric.thy
changeset 37887 2ae085b07f2f
parent 37655 f4d616d41a59
child 39910 10097e0a9dbd 
--- a/src/HOL/Word/Misc_Numeric.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -292,7 +292,7 @@
 
 (* two alternative proofs of this *)
 lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
-  apply (unfold diff_def)
+  apply (unfold diff_minus)
   apply (rule mem_same)
    apply (rule RI_minus RI_add RI_int)+
   apply simp
isabelle