Re: [isabelle-dev] Complete Distributive Lattice

That /is/ the proper way to test it. On my machine, HOL-Library takes 6 minutes of CPU time. If it takes significantly more than that on yours, there's something wrong. If it takes hours and still isn't done, there's something very wrong. Are you sure the files are processed fully and without

Re: [isabelle-dev] Complete Distributive Lattice

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

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, > wrote: > > I have a question about

[isabelle-dev] DEADLINE EXTENDED: 25th Automated Reasoning Workshop (ARW 2018), University of Cambridge, 12-13/4/18

25th AUTOMATED REASONING WORKSHOP 2018 University of Cambridge, 12-13 April 2018 http://www.cl.cam.ac.uk/events/arw2018/ CALL FOR ABSTRACTS AND STUDENT TRAVEL GRANT APPLICATIONS GENERAL INFORMATION The 25th Automated Reasoning Workshop (ARW 2018) will take place at the University of

Re: [isabelle-dev] DEADLINE EXTENDED: 25th Automated Reasoning Workshop (ARW 2018), University of Cambridge, 12-13/4/18

On 09/03/18 16:58, Dr A. Koutsoukou-Argyraki wrote: > 25th AUTOMATED REASONING WORKSHOP 2018 > > University of Cambridge, 12-13 April 2018 > http://www.cl.cam.ac.uk/events/arw2018/ Note that it does not make sense to post conference announcements here -- this is a proper subset of the