* HOL/datatype: induction rule for arbitrarily branching datatypes is
now expressed as a proper nested rule (old-style tactic scripts may
require atomize_strip_tac to cope with non-atomic premises);
* HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule
to "split_conv" (old name still available for compatibility);
* HOL: improved concrete syntax for strings (e.g. allows translation
rules with string literals);
(*
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::ringS => '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