--- 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