[isabelle] help

   Apply(simp) or by auto often is used to  prove some  theorems automatically,so we can not see the process of simplication and we only see the result of simplication.How to  show the simplification process in Proof-General ,for example the rewrite rules used by the current simplification? Is there the command?

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