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.

  then have
  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.


	Makarius


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