[isabelle-dev] Unproven class relation finite_lattice_complete < countable
makarius at sketis.net
Mon Jan 7 23:52:35 CET 2013
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.
More information about the isabelle-dev