diff -r 1d63ceb0d177 -r e5224d887e12 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 07 15:00:03 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 07 15:15:07 2012 +0200
@@ -1771,31 +1771,33 @@
 lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
   by (metis option.nchotomy)
 
-lemma exists_option:
- "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))" 
+lemma exists_option: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
   by (metis option.nchotomy)
 
-fun lifted where 
-  "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some(opp x y)" |
-  "lifted opp None _ = (None::'b option)" |
-  "lifted opp _ None = None"
+fun lifted
+where
+  "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some (opp x y)"
+| "lifted opp None _ = (None::'b option)"
+| "lifted opp _ None = None"
 
 lemma lifted_simp_1[simp]: "lifted opp v None = None"
-  apply(induct v) by auto
+  by (induct v) auto
 
 definition "monoidal opp \<equiv>  (\<forall>x y. opp x y = opp y x) \<and>
                    (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
                    (\<forall>x. opp (neutral opp) x = x)"
 
-lemma monoidalI: assumes "\<And>x y. opp x y = opp y x"
+lemma monoidalI:
+  assumes "\<And>x y. opp x y = opp y x"
   "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
   "\<And>x. opp (neutral opp) x = x" shows "monoidal opp"
   unfolding monoidal_def using assms by fastforce
 
-lemma monoidal_ac: assumes "monoidal opp"
+lemma monoidal_ac:
+  assumes "monoidal opp"
   shows "opp (neutral opp) a = a" "opp a (neutral opp) = a" "opp a b = opp b a"
   "opp (opp a b) c = opp a (opp b c)"  "opp a (opp b c) = opp b (opp a c)"
-  using assms unfolding monoidal_def apply- by metis+
+  using assms unfolding monoidal_def by metis+
 
 lemma monoidal_simps[simp]: assumes "monoidal opp"
   shows "opp (neutral opp) a = a" "opp a (neutral opp) = a"
@@ -1804,10 +1806,14 @@
 lemma neutral_lifted[cong]: assumes "monoidal opp"
   shows "neutral (lifted opp) = Some(neutral opp)"
   apply(subst neutral_def) apply(rule some_equality) apply(rule,induct_tac y) prefer 3
-proof- fix x assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
-  thus "x = Some (neutral opp)" apply(induct x) defer
+proof -
+  fix x assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
+  thus "x = Some (neutral opp)"
+    apply(induct x) defer
     apply rule apply(subst neutral_def) apply(subst eq_commute,rule some_equality)
-    apply(rule,erule_tac x="Some y" in allE) defer apply(erule_tac x="Some x" in allE) by auto
+    apply(rule,erule_tac x="Some y" in allE) defer apply(erule_tac x="Some x" in allE)
+    apply auto
+    done
 qed(auto simp add:monoidal_ac[OF assms])
 
 lemma monoidal_lifted[intro]: assumes "monoidal opp" shows "monoidal(lifted opp)"
@@ -1825,7 +1831,8 @@
 
 lemma support_clauses:
   "\<And>f g s. support opp f {} = {}"
-  "\<And>f g s. support opp f (insert x s) = (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
+  "\<And>f g s. support opp f (insert x s) =
+    (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
   "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
   "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
   "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"