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