[isabelle] Cannot interpret comm_monoid_set



Dear experts of the algebraic type class hierarchy,

I noticed that in Isabelle2016-1, it is impossible to interpret the locale comm_monoid_set because the theorem name "commute" is used both in abel_semigroup and comm_monoid_set, which is a sublocale of abel_semigroup. Consequently, the command

interpretation foo: comm_monoid_set ... ...

raises the error

Duplicate fact declaration "Scratch.foo.commute" vs. "Scratch.foo.commute"

One can get around this by first interpreting abel_semigroup with the same parameters but a different name prefix, but this is just a hack. Is it possible to rename one of the commute lemmas before the next release to avoid the clash?

Best,
Andreas





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