summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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