src/HOL/Finite_Set.thy
changeset 48632 c028cf680a3e
parent 48619 558e4e77ce69
child 48891 c0eafbd55de3
--- a/src/HOL/Finite_Set.thy	Wed Aug 01 12:14:56 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 01 15:32:36 2012 +0200
@@ -1788,7 +1788,6 @@
   with `finite A` have "finite B" by simp
   interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
   qed (simp_all add: fun_eq_iff ac_simps)
-  thm fold.comp_fun_commute' [of B b, simplified fun_eq_iff, simplified]
   from `finite B` fold.comp_fun_commute' [of B x]
     have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp
   then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute)