On Wed, 9 Feb 2011, Lawrence Paulson wrote:
I mean, let's see how many proofs are affected (including the AFP
obviously) by this proposed change. If there are many incompatibilities,
then we need to look at other ways of dealing with this issue.
What issue? This is about making a non-conservative variation of
established things, without grasping the consequences yet.
Again: Such things take a long time to understand. And as always it is a
matter of priorities where to invest time. We have many really important
reforms in the pipeline that need attention.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
