Re: [isabelle] how to know which rules to apply before apply(auto)?

On 26.10.2014 18:44, M A wrote:
> is it fact_filter to give hints about what lemma to be used? what is
> the correct command to return hints about which lemmas to be used?
Usually you just start sledgehammer (e.g., from the the sledgehammer
panel). Options like fact_filter are either for very advanced or just
internal usage.
> after tried, it seems same as giving hints about rules, however not
> lemmas.
Rules are lemmas. Or did you expect sledgehammer to suggest you a
proposition which you should prove to prove the theorem?
> Sometimes it do not have immediate response, I do not know whether it
> start or running or not start.
If you use the sledgehammer panel, there is a small rotating circle
indicating whether sledgehammer is running. If you write the
"sledgehammer" command in your theory file, it has a different
background as long as it is running.
>  "remote_vampire": Cannot connect to remote server.
You probably had no network connection, so the vampire server could not
be reached.
> "spass": Try this: by (metis list.inject) (0 ms).
Spass found a proof involving the "list.inject" lemma.
> (No structured proof available -- proof too simple.)
The proof is so simple, that sledgehammer cannot split it into more
simple steps.

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.