[isabelle-dev] Explicit behaviour of apply(auto) ?
florian.haftmann at informatik.tu-muenchen.de
Fri Oct 2 06:26:55 CEST 2009
> 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
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
Hope this helps
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 260 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev