[isabelle] 'hence' and 'thus'

[Stepan Holub]

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 by*not* 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?

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

[Tobias Nipkow]

Post by Stepan Holub

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 by*not*  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

Post by Stepan Holub
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