[isabelle] help



  hello,
   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?
                                                                         thanks
                                                                           Jean




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