[isabelle-dev] Sledgehammer proof text insertion

[Dmitriy Traytel]

Am 05.09.2013 13:35, schrieb Florian Haftmann:
> I also observed that if you use sledgehammer as old-style keyword, the
> proof text is inserted after instead of just replacing
>
>> lemma
>>    "distinct xs ⟹ n ≠ m ⟹ n < length xs ⟹ m < length xs ⟹ xs ! n ≠ xs ! m"
>>    sledgehammer by (metis distinct_conv_nth)
> But maybe in the presence of the panel it is not worth worrying about this.
The same applies to try0 for which there is no panel (yet?).

Dmitriy