Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command



On 25/11/16 12:02, Johannes HÃlzl wrote:
> Am Freitag, den 25.11.2016, 11:41 +0100 schrieb Makarius:
> 
> But 'define' is also more specific than 'obtain'. Currently the main
> difference btw 'define' and 'obtain' is that I do not need to specify a
> proof method for 'define'.
> 
> It would be nice if we do not need to provide so much redundant
> informations (two times the name of the defined constant and two times
> for each parameter...)

These Isar proof context policies are important for the purity and
clarity of the language.

In Isar 2016 there has been clarification towards proper use of Isar in
various respects. Overall, the text becomes shorter and only in a few
cases a bit longer.

I recommend to buy the whole package, and not look back on older forms.


	Makarius





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