isabelle: src/HOL/Algebra/poly/PolyHomo.thy@36a6c38e0eca (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	Universal property and evaluation homomorphism of univariate polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	$Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	Author: Clemens Ballarin, started 15 April 1997
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	6
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	7	PolyHomo = Degree +
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9	(* Instantiate result from Degree.ML *)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	10
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11	instance
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12	up :: (domain) domain (up_integral)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14	consts
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15	EVAL2 :: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16	EVAL :: 'a => 'a up => 'a
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	17
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	18	defs
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	19	EVAL2_def "EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)"
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	20	EVAL_def "EVAL == EVAL2 (%x. x)"
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	21
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	22	end

author	paulson
	Wed, 22 Dec 1999 17:18:03 +0100
changeset 8074	36a6c38e0eca
parent 7998	3d0c34795831
child 9279	fb4186e20148
permissions	-rw-r--r--