Re: [isabelle] Isar syntax question



On Fri, 25 Jul 2014, Joachim Breitner wrote:

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.

I will take a second look. That non-determinsm is probably just an accidental side-effect of generally reworked asynchronous printing in Isabelle2014-RC0.


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.

So why not change the color in Plugin Options / Isabelle / Rendering?
You should keep it somehow visible, though, otherwise the following incident might happen: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-May/msg00037.html


	Makarius


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