--- a/src/HOL/Hyperreal/StarDef.thy Thu Dec 13 07:09:09 2007 +0100
+++ b/src/HOL/Hyperreal/StarDef.thy Thu Dec 13 07:09:23 2007 +0100
@@ -933,12 +933,12 @@
done
instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono1)
+by (intro_classes, transfer, rule mult_mono1_class.less_eq_less_times_zero.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_times_zero_less_eq_less.mult_strict_mono)
+by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_less_eq_less_zero_times.mult_strict_mono)
instance star :: (pordered_ring) pordered_ring ..
instance star :: (pordered_ring_abs) pordered_ring_abs
--- a/src/HOL/Library/Multiset.thy Thu Dec 13 07:09:09 2007 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Dec 13 07:09:23 2007 +0100
@@ -959,11 +959,11 @@
mset_le_trans simp: mset_less_def)
interpretation mset_order_cancel_semigroup:
- pordered_cancel_ab_semigroup_add ["op \<le>#" "op <#" "op +"]
+ pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
interpretation mset_order_semigroup_cancel:
- pordered_ab_semigroup_add_imp_le ["op \<le>#" "op <#" "op +"]
+ pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
by (unfold_locales) simp