/usr/share/hol88-2.02.19940316/help/ENTRIES/definitions.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 29 30 31 32 33 34 | \DOC definitions
\TYPE {definitions : (string -> (string # thm) list)}
\SYNOPSIS
Returns the constant definitions, type definitions and constant specifications
of a given theory segment of the current theory.
\DESCRIBE
A call of {definitions `thy`} returns the definitions of the theory segment
{thy} together with their names. Constant definitions, type definitions and
constant specifications are all retrieved by the function {definitions}. The
theory segment {thy} must be part of the current theory. The names are those
given to the definitions by the user when they were originally added to the
theory segment (by a call, for example, to {new_definition}). The name of the
current theory segment can be abbreviated by {`-`}.
\FAILURE
The call {definitions `thy`} will fail if the theory segment {thy} is not
part of the current theory.
\EXAMPLE
{
#definitions `combin`;;
[(`I_DEF`, |- I = S K K);
(`S_DEF`, |- S = (\f g x. f x(g x)));
(`K_DEF`, |- K = (\x y. x));
(`o_DEF`, |- !f g. f o g = (\x. f(g x)))]
: (string # thm) list
}
\SEEALSO
axioms, definition, load_definition, load_definitions, new_definition, print_theory, theorems.
\ENDDOC
|