[isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa at gmail.com]

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 <lp15 at cam.ac.uk> 
Sent: Friday, March 9, 2018 12:49 PM
To: viorel.preoteasa at gmail.com
Cc: isabelle-dev at 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.preoteasa at gmail.com> <viorel.preoteasa at 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?
>