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

[Viorel Preoteasa]

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 .
> ./Coinductive/Examples/CCPO_Topology.thy
> ./Concurrent_Ref_Alg/Refinement_Lattice.thy
> ./DataRefinementIBP/Diagram.thy
> ./DataRefinementIBP/Hoare.thy
> ./DataRefinementIBP/Statements.thy
> ./LatticeProperties/Conj_Disj.thy
> ./MonoBoolTranAlgebra/Mono_Bool_Tran.thy
> ./MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy
> ./PSemigroupsConvolution/Quantales.thy
> 
> 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.

Viorel

> Larry
> 
>> 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.
>>
>