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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
