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.


A special test version for Christmas is available here:

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


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