[isabelle] More simplifier inconsistency



Dear list,

Consider the following HOL lemma:
  lemma "a ⟹ a ⟶ b ⟹ b" by simp

It is accepted by Isabelle in a plain HOL-Main environment.
However if I import Number Theory _and_ Eisbach, it is no longer accepted.
If I import just one of these (either only Main+Eisbach or
HOL-Number_Theory") it is ok.
A minimal problematic theory is attached.

Is it possible to have this lemma accepted?

Regards,
Cezary

(The attached file is loaded with 'isabelle jedit -l HOL-Number_Theory
issue.thy')

Attachment: issue.thy
Description: Binary data



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