Re: [isabelle] About auto-method
jwang whu.edu.cn (jwang) wrote:
I want to know how to print the proof procedure of auto-method in Isabelle ,for example the theroy or lemmas used by auto-method ,so I have a good understanding of the proof procedure of some theroy used in verifying security protocol.
Thanks a lot.
The procedure is found in src/Provers/clasimp.ML, under mk_auto_tac;
it contains the use of the "blast" tactics (see blast.ML) which are very
But as for the lemmas used, auto_tac uses a "claset" and a "simpset",
the reference manual (chapters 10 and 11) tell you about these. Most
commonly you would use the default ones, possibly adding rules useful
for your particular goal. So if you need to make it work better,
first try adding relevant rules. Second try alternatives - eg force_tac
This archive was generated by a fusion of
Pipermail (Mailman edition) and