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.


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.