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
The rules (and their instances) that are actually used are not immediately
tracable, due to the way the traditional lazy enumeration of potential
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and