[isabelle] Locales duplicate facts



Hi everyone,

	While I was working in HOL-Algebra, I noticed a problem in the way Isabelle deals with duplicate facts.
In the file « Divisibility.thy » there is a lemma called « Units_m_closed » (line 76).

In the file « Group. thy » , there is also a lemma called « Units_m_closed » (line 89).

The two lemmas have the same name, and Divisibility imports Group, however Isabelle is not able to spot the fact that these lemmas have the same name, and doesn’t tell the user about it.

Moreover, when you try to instantiate the monoid locale (the two lemmas are « in monoid »), Isabelle fails because of these duplicate facts.

Is there a way to deal with this problem ?

Cheers,

Martin Baillon





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