[isabelle-dev] Sledgehammer proof text insertion

Dmitriy Traytel traytel at in.tum.de
Thu Sep 5 13:41:01 CEST 2013

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?).


More information about the isabelle-dev mailing list