[isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice
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...
More information about the isabelle-dev