[isabelle-dev] Sledgehammer proof text insertion

[Florian Haftmann]

Hi,

after some time playing around with the new sledgehammer panel
(ab4edf89992f), here my feedback:

The proof text is inserted immediately after the corresponding proposition

> lemma
>   "distinct xs ⟹ n ≠ m ⟹ n < length xs ⟹ m < length xs ⟹ xs ! n ≠ xs ! m" by (metis distinct_conv_nth)

I agree with other voices that

> lemma
>   "distinct xs ⟹ n ≠ m ⟹ n < length xs ⟹ m < length xs ⟹ xs ! n ≠ xs ! m"
>   by (metis distinct_conv_nth)

is much more convenient.

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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130905/fd1d425e/attachment.asc>