[isabelle-dev] Sledgehammer proof text insertion
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
>> "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