[isabelle] Simplifier: Ignoring duplicate rewrite rule should be modulo alpha-equivalence
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?
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and