summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Algebra/UnivPoly.thy

changeset 44890 | 22f665a2e91c |

parent 44821 | a92f65e174cf |

child 49962 | a8cc904a6820 |

--- a/src/HOL/Algebra/UnivPoly.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Mon Sep 12 07:55:43 2011 +0200 @@ -105,7 +105,7 @@ 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 @@ -780,7 +780,7 @@ 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 @@ -827,7 +827,7 @@ 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" @@ -1061,7 +1061,7 @@ 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