Re: [isabelle] Unable to prove easy existential "directly"
On Fri, 19 Jul 2013, René Neumann wrote:
Am 19.07.2013 18:48, schrieb Makarius:
* 'thus' is an an old-fahsioned abbreviation,
When did this become 'old-fashioned'?
Many years ago. It goes back to an old draft of Isar, which was derived
from Mizar and the Mizar mode for HOL, before 'then' was introduced as a
standalone Isar primitive.
Did you ever wonder why there is no conflation of "then obtain"?
for people who like typing more than necessary (paradoxically).
|'th<TAB><space>sh<TAB>'| = 7
|'thus'| = 4
Not counting the time it takes to wait before autocompletion mechanisms
can be used (ie small delay before each <TAB>)
The extra typing happens when you change your structured goal
specfications back and forth several times, e.g.
from blah have
with blah have
The form with 'then' saves typing for experts and is more easy to
understand for readers of the text. Isar is very compositional by design,
more than Mizar in that respect.
This archive was generated by a fusion of
Pipermail (Mailman edition) and