Re: [isabelle] jEdit apparantly proves False

On Fri, 22 Nov 2013, Gottfried Barrow wrote:

On 11/11/2013 5:24 AM, Makarius wrote:
There's also no persistence in the "Provers" field.

The persistence is in the history of the text field. This is also useful to "park" several sets of options that are commonly used.

That's what I was talking about. In the the drop-down box, there's the string "Previously entered strings:". There's nothing ever there except for that message.

The history text field updates its history when you type RETURN into it, which then also has the effect of "Apply". The Apply button alone does not update the history.

Since the Sledgehammer panel is new, I did not have any ambitions to make it super fancy. Just plain and solid functionality.

Note that for Isabelle2013-2, I did already change the spontaneous restart behaviour of sledgehammer after editing the text:

You can try that when Isabelle2013-2-RC1 appears.


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