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.preote...@aalto.fi <mailto:viorel.preote...@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.


_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to