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

[Lawrence Paulson]

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? 

Larry

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