[isabelle-dev] Strange interaction of locales and constant definitions
noschinl at in.tum.de
Thu May 23 09:21:52 CEST 2013
On 22.05.2013 22:16, Clemens Ballarin wrote:
> This is a fairly complex interaction of structure declarations, the
> overloaded constant "pow" aka (^) and parsing of a locale expression. It
> would be interesting to see whether this problem is already present in
> early 2009 or was introduced later. HOL-Algebra has not changed much
> since 2009.
I tested the releases and it seems that this problem was introduced
between 2009-2 and 2011. It works in 2009, 2009-1 and 2009-2. It does
not work in 2011, 2012, 2013 and the current repository version. I
didn't test 2011-1.
BTW: Do you agree with me that M shouldn't be declared as structure?
More information about the isabelle-dev