On Sun, 12 Oct 2014, Makarius wrote:
On Tue, 16 Sep 2014, Makarius wrote:
On Fri, 5 Sep 2014, Jasmin Christian Blanchette wrote:
> I would like to propose either replacing the old mechanism by the new
> one
> or having both live in parallel in "Pure". It is certainly not perfect,
> but it is IMO an improvement over the statu quo. What do you think?
I still need to catch up with this important thread, but I am presently
not well-connected. I will come back later, when I have studied the
situation carefully.
I have picked up this old thread, and started to rework the old
Haftmann-Wenzel version wrt. the new Blanchette version. Stay tuned ...
See now Isabelle/4e4a4c758f9c where the old interpretation.ML is already
removed.
In the earlier changesets, the various uses of interpretation.ML and
local_interpretation.ML are converged towards the new plugin.ML -- the
main transition point is:
changeset: 58657:6c9821c32dd5
user: wenzelm
date: Mon Oct 13 18:45:48 2014 +0200
description:
Local_Interpretation is superseded by Plugin with formal Plugin_Name
management, avoiding undeclared strings;
I did not intend to push everything through in the first round, but it
worked out smoothly as far as I can see at the moment.
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
