diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Big_Operators.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -503,7 +503,7 @@
     thus ?case by simp
   next
     case insert
-    thus ?case using add_mono by fastsimp
+    thus ?case using add_mono by fastforce
   qed
 next
   case False
@@ -893,11 +893,11 @@
 
 lemma setprod_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
-by(fastsimp simp: setprod_def intro: fold_image_cong)
+by(fastforce simp: setprod_def intro: fold_image_cong)
 
 lemma strong_setprod_cong[cong]:
   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
-by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
+by(fastforce simp: simp_implies_def setprod_def intro: fold_image_cong)
 
 lemma setprod_reindex_cong: "inj_on f A ==>
     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
@@ -1590,7 +1590,7 @@
 proof -
   interpret ab_semigroup_idem_mult min
     by (rule ab_semigroup_idem_mult_min)
-  from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
+  from assms fold1_in show ?thesis by (fastforce simp: Min_def min_def)
 qed
 
 lemma Max_in [simp]:
@@ -1599,7 +1599,7 @@
 proof -
   interpret ab_semigroup_idem_mult max
     by (rule ab_semigroup_idem_mult_max)
-  from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
+  from assms fold1_in [of A] show ?thesis by (fastforce simp: Max_def max_def)
 qed
 
 lemma Min_le [simp]:
@@ -1739,8 +1739,8 @@
     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
     then have "P ?B" using `P {}` step IH[of ?B] by blast
     moreover 
-    have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
-    ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
+    have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
+    ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastforce
   qed
 qed