Ramana is right: this is a documentation bug. Michael
On 6 Dec 2013, at 4:27, "Ramana Kumar" <[email protected]<mailto:[email protected]>> wrote: Hmm... this could be a throwback to a time when the hypotheses were represented by a list... if so the documentation should be updated. I'm not entirely sure though. On Thu, Dec 5, 2013 at 5:19 PM, Rob Arthan <[email protected]<mailto:[email protected]>> wrote: Ramana assures me that HOL4 manages the assumptions of a theorem as a set modulo alpha-convertibility. I had been suspicious because of the following statement in the Reference Manual description of DISCH_ALL: "Two or more alpha-convertible hypotheses will be discharged by a single implication; users should not rely on which hypothesis appears in the implication." So is that a glitch in the documentation? Or does HOL4 offer some mysterious way of proving a theorem with two distinct but alpha-equivalent assumptions? Regards, Rob. ------------------------------------------------------------------------------ Sponsored by Intel(R) XDK Develop, test and display web and hybrid apps with a single code base. Download it for free now! http://pubads.g.doubleclick.net/gampad/clk?id=111408631&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected]<mailto:[email protected]> https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Sponsored by Intel(R) XDK Develop, test and display web and hybrid apps with a single code base. Download it for free now! http://pubads.g.doubleclick.net/gampad/clk?id=111408631&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected]<mailto:[email protected]> https://lists.sourceforge.net/lists/listinfo/hol-info ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------------------------------------------------------ Sponsored by Intel(R) XDK Develop, test and display web and hybrid apps with a single code base. Download it for free now! http://pubads.g.doubleclick.net/gampad/clk?id=111408631&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
