isabelle: src/HOL/Algebra/poly/LongDiv.thy@8e739a6eaf11 (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	Experimental theory: long division 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	Author: Clemens Ballarin, started 23 June 1999
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	LongDiv = PolyHomo +
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
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11093 diff changeset	10	lcoeff :: "'a::ring up => 'a"
7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11093 diff changeset	11	eucl_size :: 'a::ring => nat
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13	defs
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11093 diff changeset	14	lcoeff_def "lcoeff p == coeff p (deg p)"
11093 62c2e0af1d30 Changes to HOL/Algebra: ballarin parents: 7998 diff changeset	15	eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	17	end
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	18

author	obua
	Sun, 09 May 2004 23:04:36 +0200
changeset 14722	8e739a6eaf11
parent 13735	7de9342aca7a
child 14723	b77ce15b625a
permissions	-rw-r--r--