Re: [isabelle] Isar syntax question


Am Freitag, den 25.07.2014, 15:45 +0200 schrieb Makarius:
> Funnily, seasoned users stick to older habits to ignore the error 
> and turn a failed "by" into "apply" and then watch the Output window.

I try to use the "by" output, but I fail because
  a) it sometimes shows up below “have ..” and below “proof”. Before I
reach for the mouse (repeatedly, as I change my proof), I rather change
the by to apply.
 b) the red background is unpleasant to read. It makes me nervous. It
should be reserved for proper alerting. I need to be alerted once that
it’s broken, but I don’t need to be continuously alerted while working
on it.

The second point is a bit of a psychological one and might not affect
other users. OTOH, UI is nothing but psychology, so it seems to be
relevant here.

With best regards,

Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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