Re: [isabelle] A proof on moreover and ultimately



On Tue, 29 Dec 2015, Makarius wrote:

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.

See http://isabelle.in.tum.de/website-Isabelle2016-RC0


	Makarius


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