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

Clemens Ballarin 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 mailing list