HOL-Theorem-Prover/HOL — pull request #201 by xrchz (2014-10-05 14:41:22+00:00)
Title: Add gen_new_specification to the kernel.

My primary motivation here is to substantiate the claim that the new rule for HOL Constant Definition Done Right has been implemented in HOL4. In reality, there are a few loose ends but I think they can be left for later.

In particular:
* While prim_new_definition has been replaced, the old new_specification remains for use in theories before pairs are defined (because gen_new_specification uses pairs to subsume new_specification). ProofPower solves this bootstrapping problem in a way described in Arthan's paper, but leaving both rules in the kernel for now is easier.
* Also, the OpenTheory kernel and logging is not updated, but it seems to me like a) nobody uses it, and b) the OpenTheory article format is still in flux with regard to whether the new rule is primitive. I am tempted to wait and see whether an alternative implementation of proof-logging in HOL4 is worth pursuing instead (I've heard one might be coming at CPP next year).