new_constant : string * hol_type -> unit
Declares a new constant.
A call new_constant("c",`:ty`) makes c a constant with most general type
- FAILURE CONDITIONS
Fails if there is already a constant of that name in the current theory.
val it : unit = ()
Can be useful for declaring some arbitrary parameter, but more usually a
prelude to some new axioms about the constant introduced. Take care when using
- SEE ALSO
constants, new_axiom, new_definition.