<html><head></head><body>Hi Viorel,<br>
<br>
it's probably easiest to send a patch containing your changes to this mailing list. (Alternatively, a copy of all the files you changed.) Some Isabelle committer can then push this to the testboard which will run the whole AFP.<br>
<br>
Cheers<br>
Lars<br><br><div class="gmail_quote">On 27 August 2017 16:59:44 CEST, Viorel Preoteasa <viorel.preoteasa@aalto.fi> wrote:<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<pre class="k9mail">I managed to integrate the new complete distributive lattice into HOL <br />library.<br /><br />The changes are these:<br /><br />Complete_Lattice.thy<br />  - replaced the complete_distrib_lattice with the new stronger version.<br />  - moved some proofs about complete_distrib_lattice and some <br />instantiations to Hilbert_Choice<br /><br />Hilbert_Choice.thy<br />  - added all results complete_distrib_lattice, including instantiations<br />of set, fun that uses uses Hilbert choice.<br /><br />Enum.thy<br />  - new proofs that finite_3 and finite_4 are complete_distrib_lattice.<br />  - I added here the classes finite_lattice and finite_distrib_lattice<br />and proved that they are complete. This simplified quite much the proofs<br />that finite_3 and finite_4 are complete_distrib_lattice.<br /><br />Predicate.thy<br />  - new proof that predicates are complete_distrib_lattice.<br /><br />I compiled HOL in Isabelle2017-RC0 using<br /><br />isabelle build -v -c HOL<br /><br />and I got:<br /><br />Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 43.344s <br />GC time, factor 1.83)<br />Finished HOL (0:04:26 elapsed time)<br /><br />Finished at Sun Aug 27 17:41:30 GMT+3 2017<br />0:04:37 elapsed time<br /><br />But I don't now how to go from here to have these changes into Isabelle.<br /><br />There is also AFP. If there are instantiations of <br />complete_distrib_lattice, then most probably they will fail.<br /><br />One simple solution in this case could be to keep also the<br />old complete_distrib_lattice as complete_pseudo_distrib_lattice.<br /><br />Viorel<br /><br /><br />On 8/26/2017 3:06 PM, Lawrence Paulson wrote:<br /><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #729fcf; padding-left: 1ex;"><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #ad7fa8; padding-left: 1ex;"> On 25 Aug 2017, at 20:14, Viorel Preoteasa <viorel.preoteasa@aalto.fi <br /> <mailto:viorel.preoteasa@aalto.fi>> wrote:<br /><br /> One possible solution:<br /><br /> Add the new class in Complete_Lattice.thy, replacing the existing class<br /><br /> Prove the instantiations and the complete_linearord subclass later<br /> in Hilbert_Choice.<br /><br /> On the other hand, it seems inconvenient to have the Hilbert Choice<br /> to depend on so many other theories.<br /></blockquote> <br /> I’d prefer this provided the instantiations aren’t needed earlier.<br /> <br /> The delay in the introduction of the Axiom of Choice is partly <br /> historical, but it’s worth noting how much of HOL can be developed <br /> without it.<br /> <br /> Larry<br /></blockquote><hr /><br />isabelle-dev mailing list<br />isabelle-dev@in.tum.de<br /><a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br /></pre></blockquote></div></body></html>