update stateful hol syntax with new new_specification

translation to stateless not yet updated
fix definition of Const1, and make it an abbrev

previously wasn't distinguishing the type of the constant from the type
of its definition term
start on updating holSemantics for new new_specification

up to the main theorem, proves_IMP