Email Gateway (Aug 22 2022 at 18:37): Email Gateway (Aug 22 2022 at 18:37):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hello,
does this mean that the section 4.1.1. of the tutorial "Programming and
Proving in
Isabelle/HOL" is outdated?
That would be a bit unfortunate, since any new user is likely to trust
the chapter named "Isar by example" in a the first file found under
"Tutorials" in the brand new distribution.
Best
Stepan
Email Gateway (Aug 22 2022 at 18:37):From: Tobias Nipkow <nipkow@in.tum.de>
On 10/10/2018 14:47, Stepan Holub wrote:
On 7.10.2018 18:03, cl-isabelle-users-request@lists.cam.ac.uk wrote:
Isar commands 'hence' and 'thus' are merely historic: they came from
Mizar into John Harrison's Mizar mode. In very early Isar versions
(approx. 1998) I merely copied them from there. Later I refined the Isar
language quite a lot (2001/2002, 2015/2016) without reconsidering this
legacy: proofs become shorter and more maintainable bynot using
'hence' and 'thus' anymore. (That is the standard Isar style since 2006.)Hello,
does this mean that the section 4.1.1. of the tutorial "Programming and Proving in
Isabelle/HOL" is outdated?
No, these commands work fine and many users are attached to them.
Tobias
That would be a bit unfortunate, since any new user is likely to trust the
chapter named "Isar by example" in a the first file found under "Tutorials" in
the brand new distribution.Best
Stepan
Last updated: Nov 21 2024 at 12:39 UTC