Email Gateway (Aug 22 2022 at 17:12): Email Gateway (Aug 22 2022 at 17:12):From: Martin Baillon <martin.baillon@polytechnique.edu>
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
Last updated: Apr 18 2024 at 12:27 UTC