Syntax definition char

Description: Class symbol for the Hartogs function.

	Ref	Expression
Assertion	char	$$class\mathrm{har}$$