[isabelle] Simplifier: Ignoring duplicate rewrite rule should be modulo alpha-equivalence



Hi all,

I just stumbled over the following behaviour of the simplifier, which
seems to issue "ignoring duplicate rewrite rule" warnings only on
literally equivalent theorems. I would have expected (at least) alpha
equivalence here. Any reasons for the current behaviour?

-- Peter

consts 
  f :: "unit \<Rightarrow> unit"
  g :: "unit \<Rightarrow> unit"
lemma [simp]: "f x \<equiv> g x" by simp
lemma [simp]: "f y \<equiv> g y" by simp  <-- Here, I would expect a
  warning about ignored duplicate rewrite rule, but get none

lemma [simp]: "f x \<equiv> g x" by simp <-- Here, I actually get the
  warning







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