Syntax definition ctcph

Description: Function to put a norm on a pre-Hilbert space.

	Ref	Expression
Assertion	ctcph	$$class\mathrm{toCPreHil}$$