Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 'hence' and 'thus'


view this post on Zulip 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

view this post on Zulip 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

smime.p7s


Last updated: Mar 28 2024 at 08:18 UTC