| author | ballarin |
| Thu, 28 Nov 2002 10:50:42 +0100 | |
| changeset 13735 | 7de9342aca7a |
| parent 11093 | 62c2e0af1d30 |
| child 14723 | b77ce15b625a |
| permissions | -rw-r--r-- |
(* Experimental theory: long division of polynomials $Id$ Author: Clemens Ballarin, started 23 June 1999 *) LongDiv = PolyHomo + consts lcoeff :: "'a::ring up => 'a" eucl_size :: 'a::ring => nat defs lcoeff_def "lcoeff p == coeff p (deg p)" eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1" end