Based on Rob Arthan's "HOL Constant Definition Done Right". The tricky
part is deciding how and where to implement the existing definitional
rules that are theoretically subsumed by the new one.

in terms of the revised Thm.prim_specification. obviously this breaks
anything that depended on Theory.new_specification, so the next job is
to rework those things (and write a backwards-compatible version, but
later in the build sequence because it needs pairs.)

This reverts commits 7f58ad8, eae01bc, and c07a105.

Implement new_definition in terms of gen_prim_specification.
Leave the existing new_specification in place.
This plan of attack suggested by RDA.

Have only touched the standard kernel, and none of the theories.
Next steps would include updating the other kernels, implementing
new_specification in terms of gen_new_specification (at some point after
pairTheory), and removing uses of new_specification before pairTheory
one by one if possible/desired...

in pairLib - should re-export elsewhere.

Conflicts:
	src/pair/src/pairLib.sml

conflict on src/postkernel/Theory.sml, because master started checking
whether the name was valid; hopefully resolved correctly