Add DATATYPE theorems for our built-in types (sum, pair, num, option).

This makes it possible for people to get pretty-printed TeX
declarations for those types using EmitTeX. It would probably be
better engineering to store these theorems in the TypeBase, and have
them generated not just be Hol_datatype/Datatype, but also by
mk_datatype_info.