new_constant : string * hol_type -> unit
STRUCTURE
SYNOPSIS
Declares a new constant in the current theory.
DESCRIPTION
A call new_constant(n,ty) installs a new constant named n in the current theory. Note that new_constant does not specify a value for the constant, just a name and type. The constant may have a polymorphic type, which can be used in arbitrary instantiations.
FAILURE
Never fails, but issues a warning if the name is not a valid constant name. It will overwrite an existing constant with the same name in the current theory.
SEEALSO
HOL  Trindemossen-1