Declaration real_decl

Declaration. real_decl
ℝ = _

Declares the set of real numbers to be a primitive constant symbol. It is characterized by axioms rather than given by a definition.