isabelle: src/HOL/Algebra/poly/PolyRing.thy@59bc43b51aa2 (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	Instantiate polynomials to form a ring and prove further properties
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 20 January 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	PolyRing = UnivPoly +
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	instance
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	10	up :: (ring) ring
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11	(up_a_assoc, up_l_zero, up_l_neg, up_a_comm,
11093 62c2e0af1d30 Changes to HOL/Algebra: ballarin parents: 10448 diff changeset	12	up_m_assoc, up_l_one, up_l_distr, up_m_comm,
10448 da7d0e28f746 tuned; wenzelm parents: 7998 diff changeset	13	up_inverse_def, up_divide_def, up_power_def) {\| ALLGOALS (rtac refl) \|}
7998 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	nipkow
	Mon, 13 May 2002 15:27:28 +0200
changeset 13145	59bc43b51aa2
parent 11093	62c2e0af1d30
permissions	-rw-r--r--