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