author | wenzelm |
Mon, 08 May 2000 20:59:30 +0200 | |
changeset 8840 | 18b76c137c41 |
parent 7998 | 3d0c34795831 |
child 11093 | 62c2e0af1d30 |
permissions | -rw-r--r-- |
7998 | 1 |
(* |
2 |
Experimental theory: long division of polynomials |
|
3 |
$Id$ |
|
4 |
Author: Clemens Ballarin, started 23 June 1999 |
|
5 |
*) |
|
6 |
||
7 |
LongDiv = PolyHomo + |
|
8 |
||
9 |
consts |
|
10 |
lcoeff :: "'a::ringS up => 'a" |
|
11 |
eucl_size :: 'a::ringS => nat |
|
12 |
||
13 |
defs |
|
14 |
lcoeff_def "lcoeff p == coeff (deg p) p" |
|
15 |
eucl_size_def "eucl_size p == if p = <0> then 0 else deg p+1" |
|
16 |
||
17 |
end |
|
18 |