[isabelle-dev] Structures [Strange interaction of locales and constant definitions]
ballarin at in.tum.de
Mon May 27 19:15:52 CEST 2013
Quoting Lars Noschinski <noschinl at in.tum.de>:
> BTW: Do you agree with me that M shouldn't be declared as structure?
I guess, you suggest that the annotation can be removed because only
the first annotation has an effect. This is a matter of taste, and I
would prefer to keep them for reasons of symmetry. Also, it makes
refactoring easier. That is, when restructuring the declarations, one
does not spend time on inserting and deleting them along the way.
In an earlier implementation structures were indexed by numbers and
the number for the first occurrence could be omitted. After this was
changed to structure names, I have kept all structure annotations for
the above reasons.
More information about the isabelle-dev