# HG changeset patch # User haftmann # Date 1197526163 -3600 # Node ID 6067d838041a9ced5aba54e6d8a08f1f80053aa7 # Parent 97ebdbdb02995e177d87954e28b8fc0ef57c49ec changed order in class parameters diff -r 97ebdbdb0299 -r 6067d838041a src/HOL/Hyperreal/StarDef.thy --- 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 diff -r 97ebdbdb0299 -r 6067d838041a src/HOL/Library/Multiset.thy --- 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 \#" "op <#" "op +"] + pordered_cancel_ab_semigroup_add ["op +" "op \#" "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 \#" "op <#" "op +"] + pordered_ab_semigroup_add_imp_le ["op +" "op \#" "op <#"] by (unfold_locales) simp