1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
\DOC new_constant
\TYPE {new_constant : string * hol_type -> unit}
\SYNOPSIS
Declares a new constant.
\DESCRIBE
A call {new_constant("c",`:ty`)} makes {c} a constant with most general type
{ty}.
\FAILURE
Fails if there is already a constant of that name in the current theory.
\EXAMPLE
{
#new_constant("graham's_number",`:num`);;
val it : unit = ()
}
\USES
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
{new_axiom}!
\SEEALSO
constants, new_axiom, new_definition.
\ENDDOC
|
