src/HOL/Algebra/UnivPoly.thy

     from UP obtain m where boundm: "bound \<zero> m q" by fast
     have "bound \<zero> (max n m) (%i. p i \<oplus> q i)"
     proof
       fix i
       assume "max n m < i"
-      with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastsimp
+      with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastforce
     qed
     then show ?thesis ..
   qed
 qed
 

     then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
       by (unfold bound_def) fast
     then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
     then show ?thesis by (auto intro: that)
   qed
-  with deg_belowI R have "deg R p = m" by fastsimp
+  with deg_belowI R have "deg R p = m" by fastforce
   with m_coeff show ?thesis by simp
 qed
 
 lemma lcoeff_nonzero_nonzero:
   assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"

   "a \<in> carrier R ==> deg R (monom P a n) <= n"
   by (intro deg_aboveI) simp_all
 
 lemma deg_monom [simp]:
   "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
-  by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
+  by (fastforce intro: le_antisym deg_aboveI deg_belowI)
 
 lemma deg_const [simp]:
   assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
 proof (rule le_antisym)
   show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)

     from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^bsub>P\<^esub> q) 0" by simp
     also from pq have "... = \<zero>" by simp
     finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
     with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
       by (simp add: R.integral_iff)
-    with p q show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>" by fastsimp
+    with p q show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>" by fastforce
   qed
 qed
 
 theorem UP_domain:
   "domain P"