[isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice
viorel.preoteasa at aalto.fi
Sun Aug 27 19:01:00 CEST 2017
On 8/27/2017 6:11 PM, Lawrence Paulson wrote:
> 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?
They will fail only if there are instantiations of the new class, since
it is stronger. I will check these files. I discovered some files also
src/HOL/Library that need to be updated.
Some of the AFP files from this list are from my submissions.
>> On 27 Aug 2017, at 15:59, Viorel Preoteasa <viorel.preoteasa at aalto.fi
>> <mailto: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.
More information about the isabelle-dev