diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -487,7 +487,7 @@
 lemmas trancl_converseD = tranclp_converseD [to_set]
 
 lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"
-  by (fastsimp simp add: fun_eq_iff
+  by (fastforce simp add: fun_eq_iff
     intro!: tranclp_converseI dest!: tranclp_converseD)
 
 lemmas trancl_converse = tranclp_converse [to_set]
@@ -730,7 +730,7 @@
 
 lemma rel_pow_Suc_I2:
   "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
-  by (induct n arbitrary: z) (simp, fastsimp)
+  by (induct n arbitrary: z) (simp, fastforce)
 
 lemma rel_pow_0_E:
   "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
@@ -821,7 +821,7 @@
    apply (clarsimp simp: rtrancl_is_UN_rel_pow)
    apply (rule_tac x="Suc n" in exI)
    apply (clarsimp simp: rel_comp_def)
-   apply fastsimp
+   apply fastforce
   apply clarsimp
   apply (case_tac n, simp)
   apply clarsimp
@@ -942,7 +942,7 @@
 
 lemma rtrancl_finite_eq_rel_pow:
   "finite R \<Longrightarrow> R^* = (UN n : {n. n <= card R}. R^^n)"
-by(fastsimp simp: rtrancl_power dest: rel_pow_finite_bounded)
+by(fastforce simp: rtrancl_power dest: rel_pow_finite_bounded)
 
 lemma trancl_finite_eq_rel_pow:
   "finite R \<Longrightarrow> R^+ = (UN n : {n. 0 < n & n <= card R}. R^^n)"