[isabelle-dev] Complete Distributive Lattice

[Makarius]

On 27/08/17 16:59, Viorel Preoteasa wrote:
> I managed to integrate the new complete distributive lattice into HOL
> library.
> 
> The changes are these:
> 
> Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 43.344s
> GC time, factor 1.83)
> Finished HOL (0:04:26 elapsed time)
> 
> Finished at Sun Aug 27 17:41:30 GMT+3 2017
> 0:04:37 elapsed time
> 
> But I don't now how to go from here to have these changes into Isabelle.

Someone who understands Isabelle library maintenance needs to pick it up
and apply it in the proper way. This usually takes quite some time, and
exposes many unexpected problems. Main HOL is not easily changed on the
spot.


> There is also AFP.

This usually takes 2-3 more rounds of exploration.


Nothing of this is relevant for the Isabelle2017 release. When the "RC"
versions show up, it is time to finish and not to start new things.


	Makarius