[isabelle-dev] Isabelle_23-Dec-2015

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Tue Dec 29 08:56:47 CET 2015


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-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151229/1ff2a025/attachment.sig>


More information about the isabelle-dev mailing list