--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri May 20 08:16:56 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 20 11:44:16 2011 +0200
@@ -1826,8 +1826,8 @@
lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
lemma support_empty[simp]:"support opp f {} = {}" using support_subset[of opp f "{}"] by auto
-lemma fun_left_comm_monoidal[intro]: assumes "monoidal opp" shows "fun_left_comm opp"
- unfolding fun_left_comm_def using monoidal_ac[OF assms] by auto
+lemma comp_fun_commute_monoidal[intro]: assumes "monoidal opp" shows "comp_fun_commute opp"
+ unfolding comp_fun_commute_def using monoidal_ac[OF assms] by auto
lemma support_clauses:
"\<And>f g s. support opp f {} = {}"
@@ -1850,12 +1850,12 @@
proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
show ?thesis unfolding iterate_def if_P[OF True] * by auto
next case False note x=this
- note * = fun_left_comm.comp_comp_fun_commute [OF fun_left_comm_monoidal[OF assms(1)]]
+ note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
show ?thesis proof(cases "f x = neutral opp")
case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
unfolding True monoidal_simps[OF assms(1)] by auto
next case False show ?thesis unfolding iterate_def fold'_def if_not_P[OF x] support_clauses if_not_P[OF False]
- apply(subst fun_left_comm.fold_insert[OF * finite_support, simplified comp_def])
+ apply(subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
using `finite s` unfolding support_def using False x by auto qed qed
lemma iterate_some: