Re: [isabelle] Isabelle2015-RC0 available for testing
Le 04/05/2015 09:56, Makarius a Ãcrit :
> On Mon, 4 May 2015, Jasmin Blanchette wrote:
>> 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.
> There is not so much going on there. The PIDE print function for the
> auto tools merely has a hardwired policy for "theory_goal" commands,
> see also
> That may be understood as a relatively crude way to prevent the
> implicit mode from sucking up too many resources. Even in that form
> it is already quite heavy.
> Nonetheless I think that implicit tools (with good scheduling
> policies) are better than funny command-lines or click-panels. Too
> bad that we don't have 32 or 64 cores now as we should. Damn market
>> 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.
> In recent Isabelle versions the idea is to eliminate the need for
> "sorry" proofs. The document processing recovers at the next theory
What is exactly a theory command? As for now, I cannot get rid of them
in Isar proofs:
hence YYY by t
seems to be processed as "have XXX by t".
Nor on the lemma level, for example:
lemma test: "f var"
lemma "f 1"
using testby auto
Contrary to previous case "lemma 'f 1'" is not skipped. But the lemma
"test" is not defined. While this was the goal of adding a lemma (under
my workflow at least): whenever I need another lemma, I put it before
and see if it can be useful.
So what do you mean exactly by "eliminating the need for 'sorry' proofs"?
(using Isabelle RC, which is a recent Isabelle version, I assume).
> Concerning auto tools: there could be some way to mark/unmark parts of
> the proof document that should be attacked implicitly.
This archive was generated by a fusion of
Pipermail (Mailman edition) and