Syntax definition chlh

Description: Extend class notation with the final constructed Hilbert space.

	Ref	Expression
Assertion	chlh	$$class\mathrm{HLHil}$$