Hi Chantal, | I wonder if there is a mistake in the specification of the CHOOSE rule | in HOL-Light | <http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CHOOSE_UPPERCASE.html>.
Yes, indeed there is; thanks for pointing that out. I've now fixed the documentation page above. I also took the chance to propagate a few other unrelated changes from the Help/*.doc files where I hadn't kept the online html in step. | Fortunately, when I try to apply this rule in HOL-Light with the two | premisses above, I get the following error: "Exception: Failure | "CHOOSE".". That is why I conclude that the specification would be false | rather than that HOL-Light would be unsound. Yes, since the CHOOSE rule is derived from more primitive rules anyway, the correct (or at least, not too weak) side-conditions get enforced automatically by the derivation. But still, it was bad not to have the documentation right for something pretty elementary. | Perhaps in the specification, one must add that v should not be free in s? I think that is correct, and that's how I've changed the documentation. John. ------------------------------------------------------------------------------ Crystal Reports - New Free Runtime and 30 Day Trial Check out the new simplified licensing option that enables unlimited royalty-free distribution of the report engine for externally facing server and web deployment. http://p.sf.net/sfu/businessobjects _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
