Add definition for empty_v in HOL.

This takes a size, and an initial element.
Correct definition of RFOR in HOL so that it makes some sense.
Define the cpack function in HOL.

Following Michelle's definition in variants1Dloop.sml