[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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and