src/HOL/Algebra/UnivPoly.thy
changeset 26202 51f8a696cd8d
parent 23350 50c5b0912a0c
child 26934 c1ae80a58341
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Mar 05 21:24:07 2008 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Mar 05 21:33:59 2008 +0100
     1.3 @@ -1229,7 +1229,7 @@
     1.4    shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
     1.5  proof -
     1.6    interpret UP_univ_prop [R S h P s _]
     1.7 -    using `UP_pre_univ_prop R S h` P_def R S
     1.8 +    using UP_pre_univ_prop_axioms P_def R S
     1.9      by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
    1.10    from R
    1.11    show ?thesis by (rule Eval_monom)