[isabelle-dev] Issues with "interpretations"

[Makarius]

On Wed, 2 Apr 2014, Andreas Lochbihler wrote:

> If there is a duplicate declaration of a constant, one could check 
> whether the declarations of the constants are equivalent, and accept if 
> so. Since I am not familiar with the internals, I do not know whether 
> such a change is feasible in the current implementation.

That would mean to go back to ancient times where things were not 
authentic, and the system generally not very well-defined.  We've left 
this behind a long time ago.

I did not look through the list of issues in detail yet (I will do that 
later), but it is probably just a recurrence of what we knew already when 
the generic interpretation mechanism was made formal and "size" became its 
main application -- based on older less formal mechanisms.


 	Makarius