# [isabelle] Simplifier question

I wonder how to influence the precedence of simplifier rules, I have the
following problem using the Multiset library:
theory Scratch
imports Main Multiset
begin
lemma mset_singleton_eq[simp]: "a :# {#b#} = (a=b)" by auto
lemma "s:#{#f#} ==> (s=f)"
apply simp
-->This leaves me with the subgoal
0 < (if f = s then 1 else 0) ==> s = f
Of course, I could have used (simp split: split_if_asm) to resolve this,
but my point is: Why did the simplifier not use mset_singleton_eq, that
was just declared as [simp].
Examining the simplifier trace gives me, that (Multiset.count_single) is
used instead (as "x:#A" is a syntactic sugar for "0<count A x") .
Can I get the simplifier to use my lemma instead, without erasing
count_single from the default simpset ?
Bests and thanks in advance for any hints,
Peter

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*