[isabelle-dev] Explicit behaviour of apply(auto) ?

[Florian Haftmann]

Hi Mikaël,

> Can someone tell we how I can *retrieve the lemmas/rules used by
> apply(auto)* , i.e. what were the steps I should have used if I did not
> have this auto method ?
> Same question for *apply(blast)*

Although it is technically possible, it will usually waste some time and
energy to derive useful information:  display the proof term
corresponding to lemma "foo" with

	prf "foo"

Another possibility is to turn "trace simplifier" in the Isabelle
options menu in PG on before invoking simp (don't forget to turn it off
afterwards!).  This obviously will not give any hints about intro/elim
rules used during auto or blast.

Perhaps the best relevance retrieval mechanism can be found in
sledgehammer (http://isabelle.in.tum.de/sledgehammer.html).

Hope this helps
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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: 260 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091002/738eb937/attachment.sig>