equal
deleted
inserted
replaced
849 apply auto |
849 apply auto |
850 apply (rule mset_le_trans) |
850 apply (rule mset_le_trans) |
851 apply auto |
851 apply auto |
852 done |
852 done |
853 |
853 |
854 interpretation mset_order: order["op \<le>#" "op <#"] |
854 interpretation mset_order: |
855 by(auto intro: order.intro mset_le_refl mset_le_antisym mset_le_trans |
855 order ["op \<le>#" "op <#"] |
856 simp:mset_less_def) |
856 by (auto intro: order.intro mset_le_refl mset_le_antisym |
|
857 mset_le_trans simp: mset_less_def) |
857 |
858 |
858 interpretation mset_order_cancel_semigroup: |
859 interpretation mset_order_cancel_semigroup: |
859 pordered_cancel_ab_semigroup_add["op +" "op \<le>#" "op <#"] |
860 pordered_cancel_ab_semigroup_add ["op \<le>#" "op <#" "op +"] |
860 apply(unfold_locales) |
861 by unfold_locales (erule mset_le_mono_add [OF mset_le_refl]) |
861 apply(erule mset_le_mono_add[OF mset_le_refl]) |
|
862 done |
|
863 |
862 |
864 interpretation mset_order_semigroup_cancel: |
863 interpretation mset_order_semigroup_cancel: |
865 pordered_ab_semigroup_add_imp_le["op +" "op \<le>#" "op <#"] |
864 pordered_ab_semigroup_add_imp_le ["op \<le>#" "op <#" "op +"] |
866 by (unfold_locales) simp |
865 by (unfold_locales) simp |
867 |
|
868 |
866 |
869 end |
867 end |