Just a casual user experience report. In the last days I brought some ancient patches from my queue into shape (definitely nothing for the next release) and this involved a lot of proof tuning (sometimes also termination issues) scattered over many theories in the distribution and the afp. I am working on not-so-up-to-date hardware. It was quite simple to carry that out – in the past there was always a risk that a couple of non-terminating proofs would (practically) block the ui. Now I had experienced this only once. Very convincing!
Cheers,
Florian
Am 23.12.2015 um 22:55 schrieb Makarius:
> Here is another Isabelle test snapshot:
> http://www4.in.tum.de/~wenzelm/test/Isabelle_23-Dec-2015
>
> It contains an updated version of Poly/ML as an approximation of version
> 5.6 that David Matthews is preparing for the beginning of 2016.
>
> After the Christmas break, there will be further moves towards the
> Isabelle2016 release. Hopefully, Oracle will manage to keep its own
> schedule for the next Java 8 release on 19-Jan-2016:
> https://www.java.com/en/download/faq/release_dates.xml
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
