--- a/src/HOL/Algebra/poly/UnivPoly2.thy Mon Apr 07 15:37:27 2008 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Mon Apr 07 15:37:30 2008 +0200
@@ -140,9 +140,19 @@
end
-instance up :: (type) Divides.div ..
+instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") Divides.div
+begin
+
+definition "a div (b \<Colon> 'a up) = undefined a b"
+
+definition "a mod (b \<Colon> 'a up) = a - (a div b) * b"
-instantiation up :: ("{times, one, comm_monoid_add}") inverse
+instance ..
+
+end
+
+
+instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
begin
definition