On 19/11/12 11:01, Michael Norrish wrote: > Ignoring abbreviations, you could use
> fun simpterm q = > ASSUM_LIST (fn ths => Q_TAC (ASSUME_TAC o SIMP_CONV (srw_ss()) ths) q) > This simplifies the term corresponding to assumption q and gives you back the > resulting assumption. Err, this should read “corresponding to quotation q and gives you back the resulting theorem as an assumption”. Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
