[OS X TeX] times font

[Michael Sharpe]

On Oct 1, 2012, at 3:47 PM, Peter Dyballa wrote:

> 
> Am 02.10.2012 um 00:24 schrieb juan tolosa:
> 
>> What is the correct way to do it in Mac OS TeX?
> 
> ptmr8r – presumingly. That's a TeX font name for Times. "Times" seems to be some TeXtures special…
> 

TeXtures allows the use of PostScript system fonts, and Times was one such that came with the system, Instead of the low level call using \font, it might be better to use

\def\Times#1{{\fontfamily{ptm}\selectfont #1}}

and then use it in constructions like 

Is \Times{@} different from \textbf{\Times{@}}?

Michael