| changeset 9279 | fb4186e20148 |
| parent 7998 | 3d0c34795831 |
| child 11093 | 62c2e0af1d30 |
--- a/src/HOL/Algebra/poly/PolyHomo.thy Fri Jul 07 17:15:17 2000 +0200 +++ b/src/HOL/Algebra/poly/PolyHomo.thy Fri Jul 07 18:27:47 2000 +0200 @@ -13,7 +13,7 @@ consts EVAL2 :: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS - EVAL :: 'a => 'a up => 'a + EVAL :: 'a::ringS => 'a up => 'a defs EVAL2_def "EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)"