[isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

Lawrence Paulson lp15 at cam.ac.uk
Sun Aug 27 17:11:10 CEST 2017

In the AFP, grep picks up these:

~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r .

But why would they fail? The new version is surely stronger, so any changes should be pretty straightforward, right? 


> On 27 Aug 2017, at 15:59, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote:
> There is also AFP. If there are instantiations of complete_distrib_lattice, then most probably they will fail.
> One simple solution in this case could be to keep also the
> old complete_distrib_lattice as complete_pseudo_distrib_lattice.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170827/58a32214/attachment-0002.html>

More information about the isabelle-dev mailing list