[isabelle-dev] Strange interaction of locales and constant definitions

[Lars Noschinski]

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?

   -- Lars