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/String.thy
changeset 71822 67cc2319104f
parent 71535 b612edee9b0c
child 72024 9b4135e8bade 
--- a/src/HOL/String.thy	Fri May 08 06:26:27 2020 +0000
+++ b/src/HOL/String.thy	Fri May 08 06:26:28 2020 +0000
@@ -90,7 +90,7 @@
     also have \<open>\<dots> = b # map (bit a) [0..<m]\<close>
       by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps)
     finally show ?thesis
-      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps)
+      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps mod_2_eq_odd)
   qed
 qed
isabelle