munge option for disabling type abbrevs in terms \HOLtm

[dwRchyngqxs]

DO NOT merge yet! Attempt at unifying type abbreviations disabling mechanism in terms and type. Similar to the already existing -tm the syntax is -:ty. The previous type abbreviation disabling mechanism as -ty is also replaced by -:ty.

• [x] Implement -:ty parsing
• [x] Reuse and adapt code for -ty in term printing
• [x] Make it work and test it
• [ ] Update documentation
• [ ] Update tests