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/IMP/Abs_Int1_parity.thy
changeset 64593 50c715579715
parent 61890 f6ded81f5690
child 67406 23307fd33906 
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -112,7 +112,8 @@
   case 3 show ?case by auto
 next
   case (4 _ a1 _ a2) thus ?case
-    by (induction a1 a2 rule: plus_parity.induct) (auto simp add:mod_add_eq)
+    by (induction a1 a2 rule: plus_parity.induct)
+      (auto simp add: mod_add_eq [symmetric])
 qed
 
 text{* In case 4 we needed to refer to particular variables.
isabelle