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