# HG changeset patch
# User wenzelm
# Date 1347019123 -7200
# Node ID 85116a86d99f600d66a7c3719fc07c53021fa942
# Parent  d383fd5dbd3c5b89b534b5f91f510f46ca896520
tuned proofs;

diff -r d383fd5dbd3c -r 85116a86d99f src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 07 08:36:04 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 07 13:58:43 2012 +0200
@@ -3989,7 +3989,7 @@
 
 lemma has_integral_spike_set_eq: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach" 
   assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
-  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by (safe, auto split: split_if_asm)
+  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by (auto split: split_if_asm)
 
 lemma has_integral_spike_set[dest]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
   assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"