[isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

2017-08-29 Thread Manuel Eberl
Is it intentional that the "Computational_Algebra" theory does not import "Polynomial_Factorial"? Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the Isabelle2017 release

2017-08-29 Thread Makarius
On 24/08/17 17:40, Florian Haftmann wrote: > > Hence that change should be fine if someone is willing to undertake it > before the RC stabilization phase. We are already in stabilization phase for some weeks. There are a few days left until Isabelle2017-RC1 (presumably on 03-Sep-2017) to make

[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

2017-08-29 Thread Clemens Ballarin
On 2017-08-24 09:38, Thiemann, Rene wrote: If one imports HOL-Algebra.Multiplicative_Group (which we actually do via some transitive import), then \mu (LFP), \nu (GFP) and \phi (Euler’s totient function) become constants. Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.

Re: [isabelle-dev] Complete Distributive Lattice

2017-08-29 Thread Viorel Preoteasa
OK, I understand, what is the time frame for going back to normal? I did spent some time on this and I would like to see it finished. As I mentioned earlier, I added finite lattices to simplify the proofs in Enum.thy that finite_n are distributive complete lattices. However, searching for

Re: [isabelle-dev] Complete Distributive Lattice

2017-08-29 Thread Makarius
On 28/08/17 20:26, Viorel Preoteasa wrote: > OK, I understand, what is the time frame for going back to normal? This is hard to say, since official Isabelle2017-RC1 is not even there yet, but it is planned for Sun 03-Sep-2017. The final lift off will probably take 6 weeks from Isabelle2017-RC1,

Re: [isabelle-dev] Complete Distributive Lattice

2017-08-29 Thread Lawrence Paulson
For sure. The work is very welcome, but too drastic to undertake at this precise moment. Larry > On 28 Aug 2017, at 13:08, Makarius wrote: > > Nothing of this is relevant for the Isabelle2017 release. When the "RC" > versions show up, it is time to finish and not to start

Re: [isabelle-dev] Complete Distributive Lattice

2017-08-29 Thread Makarius
On 27/08/17 16:59, Viorel Preoteasa wrote: > I managed to integrate the new complete distributive lattice into HOL > library. > > The changes are these: > > Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 43.344s > GC time, factor 1.83) > Finished HOL (0:04:26 elapsed time) > >