changeset 73535 | 0f33c7031ec9 |
parent 72619 | 4b2691211719 |
child 74101 | d804e93ae9ff |
--- a/src/HOL/Groups_List.thy Mon Apr 05 22:46:41 2021 +0200 +++ b/src/HOL/Groups_List.thy Tue Apr 06 18:12:20 2021 +0000 @@ -430,7 +430,8 @@ 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 mod_2_eq_odd) + using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps) + (simp_all add: ac_simps mod_2_eq_odd) qed qed