# HG changeset patch
# User haftmann
# Date 1193426539 -7200
# Node ID 1a7318a040686408596bd3d9395a2f92d3eafc2d
# Parent  d58c14280367feb9a7fe42a08dc767e1739185cc
changed order of class parameters

diff -r d58c14280367 -r 1a7318a04068 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Fri Oct 26 21:22:18 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Oct 26 21:22:19 2007 +0200
@@ -403,12 +403,12 @@
 done
 
 instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.less_eq_less_times_zero.mult_mono)
+by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono)
 
 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_mono)
+by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)
 
 instance star :: (pordered_ring) pordered_ring ..
 instance star :: (lordered_ring) lordered_ring ..
diff -r d58c14280367 -r 1a7318a04068 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Oct 26 21:22:18 2007 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Oct 26 21:22:19 2007 +0200
@@ -851,19 +851,17 @@
  apply auto
 done
 
-interpretation mset_order: order["op \<le>#" "op <#"]
-by(auto intro: order.intro mset_le_refl mset_le_antisym mset_le_trans
-        simp:mset_less_def)
+interpretation mset_order:
+  order ["op \<le>#" "op <#"]
+  by (auto intro: order.intro mset_le_refl mset_le_antisym
+    mset_le_trans simp: mset_less_def)
 
 interpretation mset_order_cancel_semigroup:
-  pordered_cancel_ab_semigroup_add["op +" "op \<le>#" "op <#"]
-apply(unfold_locales)
-apply(erule mset_le_mono_add[OF mset_le_refl])
-done
+  pordered_cancel_ab_semigroup_add ["op \<le>#" "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 \<le>#" "op <#"]
-by (unfold_locales) simp
-
+  pordered_ab_semigroup_add_imp_le ["op \<le>#" "op <#" "op +"]
+  by (unfold_locales) simp
 
 end