src/HOL/Multivariate_Analysis/Integration.thy
changeset 42869 43b0f61f56d0
parent 41969 1cf3e4107a2a
child 42871 1c0b99f950d9
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 08:16:13 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 08:16:56 2011 +0200
     1.3 @@ -1850,12 +1850,12 @@
     1.4  proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
     1.5    show ?thesis unfolding iterate_def if_P[OF True] * by auto
     1.6  next case False note x=this
     1.7 -  note * = fun_left_comm.fun_left_comm_apply[OF fun_left_comm_monoidal[OF assms(1)]]
     1.8 +  note * = fun_left_comm.comp_comp_fun_commute [OF fun_left_comm_monoidal[OF assms(1)]]
     1.9    show ?thesis proof(cases "f x = neutral opp")
    1.10      case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
    1.11        unfolding True monoidal_simps[OF assms(1)] by auto
    1.12    next case False show ?thesis unfolding iterate_def fold'_def  if_not_P[OF x] support_clauses if_not_P[OF False]
    1.13 -      apply(subst fun_left_comm.fold_insert[OF * finite_support])
    1.14 +      apply(subst fun_left_comm.fold_insert[OF * finite_support, simplified comp_def])
    1.15        using `finite s` unfolding support_def using False x by auto qed qed 
    1.16  
    1.17  lemma iterate_some: