| author | kleing |
| Tue, 13 May 2003 08:59:21 +0200 | |
| changeset 14024 | 213dcc39358f |
| parent 13735 | 7de9342aca7a |
| 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