/usr/share/hol88-2.02.19940316/help/ENTRIES/constants.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | \DOC constants
\TYPE {constants : (string -> term list)}
\SYNOPSIS
Returns a list of the constants defined in a named theory.
\DESCRIBE
The call
{
constants `thy`
}
\noindent where {thy} is an ancestor theory (the special string {`-`} means the
current theory), returns a list of all the constants in that theory.
\FAILURE
Fails if the named theory does not exist, or is not an ancestor of the
current theory.
\EXAMPLE
{
#constants `combin`;;
["I"; "S"; "K"; "$o"] : term list
}
\SEEALSO
axioms, binders, definitions, infixes, theorems
\ENDDOC
|