[isabelle] What auto actually can do

Hi all,

I have a quick question about what auto actually can do. On page 72 in the
tutorial, the proof for imp_uncurry seems to use only natural deduction. How
come the user needs to manually decide each step and not use auto for it?
What rules does auto actually have and what can/can't it do?

Thanks for the help.


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