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

Mikaël Mayer mmikael222 at gmail.com
Wed Sep 30 15:59:26 CEST 2009


Hi everybody !

I'm completely new in Isabelle, so sorry if I ask trivial questions.
However, I went through the tutorial and could not manage to find the answer
for this one.

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)*

Thanks !
Mikaël Mayer
EPFL Master Student
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090930/3cdf8d16/attachment.html>


More information about the isabelle-dev mailing list