Re: [isabelle] Isar syntax question



On Thu, 17 Jul 2014, Joachim Breitner wrote:

it would be very helpful, especially for beginners, but often also for me, if a "proof" would tell us what rule it applied – similar to how "also" tells us what the current calculation is.

(And while are are at it: "also" could also tell us what rule it used...)

The rules (and their instances) that are actually used are not immediately tracable, due to the way the traditional lazy enumeration of potential results works.

I have often reconsidered that, but the only reform that went through in recent years was better error reporting in the absence of results -- instead of just "empty result sequence". Thus users merely need to look at the error message of some failed "by ..." command or calculational step. Funnily, seasoned users stick to older habits to ignore the error and turn a failed "by" into "apply" and then watch the Output window.

There is now also a *tiny* reform in the printing of 'also' / 'finally' for Isabelle2014 -- to discontinue some old workarounds for TTY interaction.


	Makarius


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