diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -650,7 +650,7 @@
   finally have linv: "\<one> = c \<otimes> b" .
 
   from ccarr linv[symmetric] rinv[symmetric]
-  have "b \<in> Units G" unfolding Units_def by fastsimp
+  have "b \<in> Units G" unfolding Units_def by fastforce
   with nunit
       show "False" ..
 qed
@@ -710,8 +710,8 @@
   fixes G (structure)
   shows "properfactor G = lless (division_rel G)"
 apply (rule ext) apply (rule ext) apply rule
- apply (fastsimp elim: properfactorE2 intro: weak_llessI)
-apply (fastsimp elim: weak_llessE intro: properfactorI2)
+ apply (fastforce elim: properfactorE2 intro: weak_llessI)
+apply (fastforce elim: weak_llessE intro: properfactorI2)
 done
 
 lemma (in monoid) properfactor_cong_l [trans]:
@@ -751,26 +751,26 @@
     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G (c \<otimes> a) (c \<otimes> b)"
 using ab carr
-by (fastsimp elim: properfactorE intro: properfactorI)
+by (fastforce elim: properfactorE intro: properfactorI)
 
 lemma (in monoid_cancel) properfactor_mult_l [simp]:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b"
 using carr
-by (fastsimp elim: properfactorE intro: properfactorI)
+by (fastforce elim: properfactorE intro: properfactorI)
 
 lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
   assumes ab: "properfactor G a b"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G (a \<otimes> c) (b \<otimes> c)"
 using ab carr
-by (fastsimp elim: properfactorE intro: properfactorI)
+by (fastforce elim: properfactorE intro: properfactorI)
 
 lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b"
 using carr
-by (fastsimp elim: properfactorE intro: properfactorI)
+by (fastforce elim: properfactorE intro: properfactorI)
 
 lemma (in monoid) properfactor_prod_r:
   assumes ab: "properfactor G a b"
@@ -1811,7 +1811,7 @@
   assumes "x \<in> carrier G"
   shows "x \<in> assocs G x"
 using assms
-by (fastsimp intro: closure_ofI2)
+by (fastforce intro: closure_ofI2)
 
 lemma (in monoid) assocs_repr_independenceD:
   assumes repr: "assocs G x = assocs G y"
@@ -2007,7 +2007,7 @@
 
   from tm as'carr[THEN subsetD] bscarr[THEN subsetD]
   have "as' [\<sim>] bs"
-    by (induct as' arbitrary: bs) (simp, fastsimp dest: assocs_eqD[THEN associated_sym])
+    by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
 
   from tp and this
     show "essentially_equal G as bs" by (fast intro: essentially_equalI)
@@ -3451,7 +3451,7 @@
       by (intro ih[of a']) simp
 
   hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
-    apply (elim essentially_equalE) apply (fastsimp intro: essentially_equalI)
+    apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)
   done
 
   from carr