Re: [isabelle] Isabelle2015-RC0 available for testing

> Have you tried playing with âAuto Sledgehammerâ and friends? You can enable them in the Isabelle plugin options and adjust their timeouts.

I should perhaps add for clarification that Auto Sledgehammer, like the other auto tools, works fine for top-level lemmas but not for subgoals or intermediate steps in an Isar proof. This is something that would require more work in Isabelle/jEdit.

For starters, it would be nice if Isabelle/jEdit could notice âsorryâs and attack them. I donât think Iâm the only one who introduces them regularly as placeholders to prevent the interface from showing errors.


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