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/SPARK/Examples/RIPEMD-160/Round.thy
changeset 55818 d8b2f50705d0
parent 45546 6dd3e88de4c2
child 56798 939e88e79724 
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Mar 01 09:34:08 2014 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Mar 01 17:08:39 2014 +0100
@@ -456,7 +456,7 @@
     unfolding round_def
     unfolding steps_to_steps'
     unfolding H1[symmetric]
-    by (simp add: uint_word_ariths(2) rdmods
+    by (simp add: uint_word_ariths(1) rdmods
       uint_word_of_int_id)
 qed
isabelle