[isabelle-dev] Unproven class relation finite_lattice_complete < countable

[Makarius]

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