| author | nipkow |
| Mon, 13 May 2002 15:27:28 +0200 | |
| changeset 13145 | 59bc43b51aa2 |
| parent 11093 | 62c2e0af1d30 |
| child 13735 | 7de9342aca7a |
| permissions | -rw-r--r-- |
(* Experimental theory: long division of polynomials $Id$ Author: Clemens Ballarin, started 23 June 1999 *) LongDiv = PolyHomo + consts lcoeff :: "'a::ringS up => 'a" eucl_size :: 'a::ringS => nat defs lcoeff_def "lcoeff p == coeff (deg p) p" eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1" end