<div dir="ltr">My changes to Complete Distributive Lattices are now integrated in the development version of Isabelle.<div><br></div><div>I want to thank Manuel Eberl for helping with testing and pushing the update into repository.</div><div><br></div><div>Viorel Preoteasa</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 9, 2018 at 12:48 PM, Lawrence Paulson <span dir="ltr"><<a href="mailto:lp15@cam.ac.uk" target="_blank">lp15@cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I don’t think it’s a problem that your more general theorems require the Axiom of Choice, and Hilbert_Choice.thy is not too large already (far from it).<br>
<br>
Larry Paulson<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
> On 8 Mar 2018, at 21:35, <<a href="mailto:viorel.preoteasa@gmail.com">viorel.preoteasa@gmail.com</a>> <<a href="mailto:viorel.preoteasa@gmail.com">viorel.preoteasa@gmail.com</a>> wrote:<br>
><br>
> I have a question about how to organize these changes. The problem is that most of the results for the more general lattice (instantiations<br>
> to set, fun) require Hilbert_Choice which is not available in Complete_Lattice. Now I have added all results about complete distributive<br>
> lattices that need Hilbert Choice in Hilbert_Choice.thy. Is this acceptable?<br>
><br>
<br>
</div></div></blockquote></div><br></div>