[isabelle-dev] Issues with "interpretations"
makarius at sketis.net
Wed Apr 2 17:06:16 CEST 2014
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.
More information about the isabelle-dev