author | wenzelm |
Mon, 08 May 2000 20:59:30 +0200 | |
changeset 8840 | 18b76c137c41 |
parent 7998 | 3d0c34795831 |
child 9279 | fb4186e20148 |
permissions | -rw-r--r-- |
(* Universal property and evaluation homomorphism of univariate polynomials $Id$ Author: Clemens Ballarin, started 15 April 1997 *) PolyHomo = Degree + (* Instantiate result from Degree.ML *) instance up :: (domain) domain (up_integral) consts EVAL2 :: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS EVAL :: 'a => 'a up => 'a defs EVAL2_def "EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)" EVAL_def "EVAL == EVAL2 (%x. x)" end