[isabelle] isabelle help



Hi,

 

I am doing some study on Isabelle.  I have these questions.  If anyone could help me with this that would be great.

 

ML {* print_cs(claset()) *}

The command above prints out all rules that are used in finding the proof including failed ones.  Is there a command which prints out only the successful ones?

 

The other question was :  Can we prove equalities and inequalities using Isabelle?  If so how?  Can you please guide me?

 

Thanks,

 

 

Kumar Chandran

 

This electronic message contains information from CTIS, Inc., which may be company sensitive, proprietary, privileged or otherwise protected from disclosure. The information is intended to be used solely by the recipients named above. If you are not an intended recipient, be aware that any review,disclosure, copying, distribution or use of this transmission or its contents is prohibited. If you have received this transmission in error, please notify us immediately at ITM at ctisinc.com.



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