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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
