| changeset 13735 | 7de9342aca7a |
| parent 11093 | 62c2e0af1d30 |
| child 14723 | b77ce15b625a |
--- a/src/HOL/Algebra/poly/LongDiv.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/poly/LongDiv.thy Thu Nov 28 10:50:42 2002 +0100 @@ -7,11 +7,11 @@ LongDiv = PolyHomo + consts - lcoeff :: "'a::ringS up => 'a" - eucl_size :: 'a::ringS => nat + lcoeff :: "'a::ring up => 'a" + eucl_size :: 'a::ring => nat defs - lcoeff_def "lcoeff p == coeff (deg p) p" + lcoeff_def "lcoeff p == coeff p (deg p)" eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1" end