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
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
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.
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
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,
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
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)
>
>