>> Do you (or anyone) know if there is a way to do this in HOL Light? > > Looking at HOL Light's kernel briefly I think the only thing you can > do is call new_axiom a lot How about making assumptions? Then at the end you just have to check that your theorems have no unwanted assumptions...
------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
