Hi everyone, I've written a utility for refactoring HOL Light tactic proofs, called Tactician and available here: http://www.proof-technologies.com/tactician/index.html This page includes download, installation instructions and example usage.
It is loaded into a normal HOL Light session, and records proofs internally as they are executed and outputs refactored versions upon user request. Refactoring operations include: - packaging up a tactic proof into a single tactic using THEN and THENL; - flattening out a packaged-up proof into a series of single-tactic steps. Flattening out is particularly useful for those wishing learn from the hundreds of packaged-up proofs that come with the HOL Light release. Mark ------------------------------------------------------------------------------ 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
