/usr/share/hol88-2.02.19940316/help/ENTRIES/binders.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 binders
\TYPE {binders : (string -> term list)}
\SYNOPSIS
Lists the binders in the named theory.
\DESCRIBE
The function {binders} should be applied to a string which is the name of an
ancestor theory (including the current theory; the special string {`-`} is
always interpreted as the current theory). It returns a list of all the binders
declared in the named theory.
\FAILURE
Fails unless the given theory is an ancestor of the current theory.
\EXAMPLE
{
#binders `bool`;;
["$?!"; "$!"; "$@"] : term list
#binders `ind`;;
[] : term list
}
\SEEALSO
ancestors, axioms, constants, definitions, infixes, new_binder, parents, types.
\ENDDOC
|