src/HOL/Algebra/UnivPoly.thy
changeset 44655 fe0365331566
parent 38131 df8fc03995a4
child 44821 a92f65e174cf
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Sep 02 17:58:32 2011 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Sep 02 18:17:45 2011 +0200
     1.3 @@ -1764,7 +1764,7 @@
     1.4      and deg_r_0: "deg R r = 0"
     1.5      shows "r = monom P (eval R R id a f) 0"
     1.6  proof -
     1.7 -  interpret UP_pre_univ_prop R R id P proof qed simp
     1.8 +  interpret UP_pre_univ_prop R R id P by default simp
     1.9    have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
    1.10      using eval_ring_hom [OF a] by simp
    1.11    have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"