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