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/Word.thy
changeset 25162 ad4d5365d9d8
parent 25134 3d4953e88449
child 25595 6c48275f9c76 
--- a/src/HOL/Library/Word.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Word.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -479,7 +479,7 @@
         with mod_div_equality [of n 2]
         show "n div 2 * 2 = n" by simp
       next
-        assume "n mod 2 \<noteq> 0"
+        assume "n mod 2 = Suc 0"
         with mod_div_equality [of n 2]
         show "Suc (n div 2 * 2) = n" by arith
       qed
isabelle