isabelle: src/HOL/Algebra/poly/Degree.thy@18b76c137c41 (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	Degree of 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	written by Clemens Ballarin, started 22. 1. 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	Degree = PolyRing +
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	consts
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	10	deg :: ('a::ringS) up => nat
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12	defs
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13	deg_def "deg p == LEAST n. bound n (Rep_UP p)"
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15	end

author	wenzelm
	Mon, 08 May 2000 20:59:30 +0200
changeset 8840	18b76c137c41
parent 7998	3d0c34795831
permissions	-rw-r--r--