Re: [isabelle] Isabelle2013-RC2 available for testing

On Mon, 28 Jan 2013, Gottfried Barrow wrote:

The cycle is something like this:

1) Start Sledgehammer.

2) Hover over "sledgehammer".

3) When the tooltip window pops up, click on the "Detach tooltip window" icon so that it's a normal window and doesn't disappear if I click somewhere else.

4) Scroll to the bottom to see if there's any new output there to think about, and maybe go ahead and click on a proof to insert it and terminate Sledgehammer.

5) Close the window.

6) Loop through items 2 through 5 until sledgehammer finishes, and then do it one last time.

Yes, this is approaching a good way to do it. A minor technical snag remains: the tooltip is not updated dynamically, and this won't happen for Isabelle2013.


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