Re: [isabelle] A proof on moreover and ultimately



On Tue, 29 Dec 2015, Manuel Eberl wrote:

I would like to add that this looks like a classic use case of Isabelle2016's âconsiderâ syntax. This approach avoids the âbig bang integrationâ at the end.

Indeed.

A special test version for Christmas is available here: http://www4.in.tum.de/~wenzelm/test/Isabelle_23-Dec-2015/

Official release candidates for Isabelle2016 will be published next year; stay tuned.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.