Hi, I'm using EmitTeX to convert a HOL theorem into a TeX string, the function print_theorem_as_tex generates a token: \HOLTokenEquiv. Which package should I add in order for Tex to recognize this command except holtexbasic and holtex? Where to get it?
Thanks. Lu ------------------------------------------------------------------------------ Create and Deploy Rich Internet Apps outside the browser with Adobe(R)AIR(TM) software. With Adobe AIR, Ajax developers can use existing skills and code to build responsive, highly engaging applications that combine the power of local resources and data with the reach of the web. Download the Adobe AIR SDK and Ajax docs to start building applications today-http://p.sf.net/sfu/adobe-com _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
