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]> 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]
> 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]
https://lists.sourceforge.net/lists/listinfo/hol-info
