Dear list, please find at https://github.com/aravantv/impconv the new version of my "implicational conversion" library for HOL Light.
It provides: - many efficiency improvements and broader applications of IMP_REWRITE_TAC (this tactic that I discussed a few times here, which takes a theorem of the form P ==> l = r and replaces l by r in a goal adding whatever it needs to make it work properly -- typically conjunction with P; but can also be an implication or even existentials) - a new tactic called TARGET_REWRITE_TAC which is useful basically anytime you need to rewrite a theorem in a precise location or with a theorem which makes the rewriting diverge. These two tactics, their use cases, and how they improve a lot over existing tactics is described in details in the user manual. In practice, these two tactics are so useful that many proofs happen to be only combinations of them. To demonstrate this, we provide a complete rewriting of a complex functions spaces library written by Mohamed Yousri Mahmoud and myself (which was presented at NFM2013) in the directory "example". Regards, -- Vincent Aravantinos, PhD Analysis and Design of Dependable Systems fortiss GmbH <www.fortiss.org/en> Guerickestrasse 25 | 80805 Munich | Germany ------------------------------------------------------------------------------ October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60133471&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
