src/HOL/List.thy
changeset 49739 13aa6d8268ec
parent 48891 c0eafbd55de3
child 49757 73ab6d4a9236
     1.1 --- a/src/HOL/List.thy	Mon Oct 08 11:37:03 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Oct 08 12:03:49 2012 +0200
     1.3 @@ -2398,7 +2398,7 @@
     1.4    assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     1.5      and x: "x \<in> set xs"
     1.6    shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
     1.7 -  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
     1.8 +  using assms by (induct xs) (auto simp add: comp_assoc)
     1.9  
    1.10  lemma fold_cong [fundef_cong]:
    1.11    "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)