| author | paulson |
| Fri, 15 Aug 2003 13:45:39 +0200 | |
| changeset 14151 | b8bb6a6a2c46 |
| 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