diff -r 48b8d8b8334d -r 2d83f93c3580 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 07 08:03:46 2006 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 07 09:33:47 2006 +0100
@@ -361,7 +361,9 @@
 apply (transfer, rule right_distrib)
 done
 
-instance star :: (semiring_0) semiring_0 ..
+instance star :: (semiring_0) semiring_0 
+by intro_classes (transfer, simp)+
+
 instance star :: (semiring_0_cancel) semiring_0_cancel ..
 
 instance star :: (comm_semiring) comm_semiring
@@ -417,7 +419,7 @@
 done
 
 instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule pordered_comm_semiring_class.mult_mono)
+by (intro_classes, transfer, rule mult_mono1_class.mult_mono)
 
 instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..