--- a/src/HOL/NSA/StarDef.thy Fri Aug 29 07:43:25 2008 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Aug 29 08:14:58 2008 +0200
@@ -824,7 +824,7 @@
by (intro_classes, transfer, rule mult_commute)
instance star :: (comm_monoid_add) comm_monoid_add
-by (intro_classes, transfer, rule comm_monoid_add_class.zero_plus.add_0)
+by (intro_classes, transfer, rule comm_monoid_add_class.add_0)
instance star :: (monoid_mult) monoid_mult
apply (intro_classes)
@@ -941,12 +941,12 @@
done
instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.less_eq_less_times_zero.mult_mono1)
+by (intro_classes, transfer, rule mult_mono1_class.mult_mono1)
instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict
-by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_less_eq_less_zero_times.mult_strict_left_mono_comm)
+by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.mult_strict_left_mono_comm)
instance star :: (pordered_ring) pordered_ring ..
instance star :: (pordered_ring_abs) pordered_ring_abs