src/HOL/Algebra/UnivPoly.thy
changeset 44890 22f665a2e91c
parent 44821 a92f65e174cf
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4      proof
     1.5        fix i
     1.6        assume "max n m < i"
     1.7 -      with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastsimp
     1.8 +      with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastforce
     1.9      qed
    1.10      then show ?thesis ..
    1.11    qed
    1.12 @@ -780,7 +780,7 @@
    1.13      then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
    1.14      then show ?thesis by (auto intro: that)
    1.15    qed
    1.16 -  with deg_belowI R have "deg R p = m" by fastsimp
    1.17 +  with deg_belowI R have "deg R p = m" by fastforce
    1.18    with m_coeff show ?thesis by simp
    1.19  qed
    1.20  
    1.21 @@ -827,7 +827,7 @@
    1.22  
    1.23  lemma deg_monom [simp]:
    1.24    "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
    1.25 -  by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
    1.26 +  by (fastforce intro: le_antisym deg_aboveI deg_belowI)
    1.27  
    1.28  lemma deg_const [simp]:
    1.29    assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
    1.30 @@ -1061,7 +1061,7 @@
    1.31      finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
    1.32      with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
    1.33        by (simp add: R.integral_iff)
    1.34 -    with p q show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>" by fastsimp
    1.35 +    with p q show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>" by fastforce
    1.36    qed
    1.37  qed
    1.38