In the AFP, grep picks up these:

~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r .

But why would they fail? The new version is surely stronger, so any changes 
should be pretty straightforward, right? 


> On 27 Aug 2017, at 15:59, Viorel Preoteasa <> 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

Reply via email to