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
