# HG changeset patch
# User haftmann
# Date 1207575450 -7200
# Node ID 420567ad81251e3d8773db2f1febab505f152d5f
# Parent  9d25ef112cf6db3cc654ac957c14a2769ee0cfe8
explicit dummy instantiation for div

diff -r 9d25ef112cf6 -r 420567ad8125 src/HOL/Algebra/poly/UnivPoly2.thy
--- 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