src/HOL/Library/RBT_Set.thy
changeset 57514 bdc2c6b40bf2
parent 56790 f54097170704
child 57816 d8bbb97689d3
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -657,7 +657,7 @@
     1.4  lemma setsum_Set [code]:
     1.5    "setsum f (Set xs) = fold_keys (plus o f) xs 0"
     1.6  proof -
     1.7 -  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
     1.8 +  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
     1.9    then show ?thesis 
    1.10      by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
    1.11  qed