Hello, I am looking for an alternative of WF_INDUCT_TAC for HOL4. I would be greatful if someone can provide good advice. I found a link for this tactic but the code is for hol_light.
http://mws.cs.ru.nl/~mptp/hol-flyspeck/trunk/wf.html Looking forward to your response. Thank you. Regards Qasim ------------------------------------------------------------------------------ Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server from Actuate! Instantly Supercharge Your Business Reports and Dashboards with Interactivity, Sharing, Native Excel Exports, App Integration & more Get technology previously reserved for billion-dollar corporations, FREE http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
