Syntax definition chft

Description: Extend class notation with scalar product of Hilbert space functional.

	Ref	Expression
Assertion	chft	$$class{·}_{\mathrm{fn}}$$