src/HOL/NSA/StarDef.thy
changeset 27651 16a26996c30e
parent 27468 0783dd1dc13d
child 27682 25aceefd4786
--- a/src/HOL/NSA/StarDef.thy	Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/NSA/StarDef.thy	Fri Jul 18 18:25:53 2008 +0200
@@ -531,6 +531,8 @@
 
 end
 
+instance star :: (Ring_and_Field.dvd) Ring_and_Field.dvd ..
+
 instantiation star :: (Divides.div) Divides.div
 begin