I am trying to test HOL-Library by using: ./bin/isabelle build -v HOL-Library
But it takes very long. It has now been working for few hours, and it is still running. I also tried to open all files from HOL/Library in Isabelle/jedit and they were processed quite fast, without any errors. What is the appropriate way to test HOL-Library? Viorel Preoteasa -----Original Message----- From: Lawrence Paulson <l...@cam.ac.uk> Sent: Friday, March 9, 2018 12:49 PM To: viorel.preote...@gmail.com Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de Subject: Re: [isabelle-dev] Complete Distributive Lattice 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). Larry Paulson > On 8 Mar 2018, at 21:35, <viorel.preote...@gmail.com> > <viorel.preote...@gmail.com> wrote: > > I have a question about how to organize these changes. The problem is > that most of the results for the more general lattice (instantiations > to set, fun) require Hilbert_Choice which is not available in > Complete_Lattice. Now I have added all results about complete distributive > lattices that need Hilbert Choice in Hilbert_Choice.thy. Is this acceptable? > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
