On Mon, 7 Jan 2013, Makarius wrote:
On Sat, 29 Dec 2012, Florian Haftmann wrote:
> So far. I will stop for today, and I am not sure when I am able to turn
> back on the issue. But maybe I have found enough that the original
> authors can comment on it.
Yet an even more minimal example
I will study this a bit further ...
The current result is 2bbc7ae80634, where I have reworked the transitive
closure a bit -- following similar things I've done recently with the
Graph module (68c9a6538c0e and 2e22cdccdc38). At some point one needs to
sit down an formalize all that properly -- but here it is again not
directly relevant for the correctnes of the inference kernel.
There was a quite different surprise with stale theories during
Thm.close_derivation: it needs to be done sequentially if the current the
current theory is a draft (unstable): storing more proven classrels in the
theory concurrently could cause a crash.
Lets see how this works in the next few days.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
