/usr/share/hol88-2.02.19940316/help/ENTRIES/parents.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 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 | \DOC parents
\TYPE {parents : (string -> string list)}
\SYNOPSIS
Lists the parent theories of a named theory.
\DESCRIBE
The function {parents} returns a list of strings that identify the
parent theories of a named theory. The function does not recursively
descend the theory hierarchy in search of the `leaf' theories.
The named theory must be the current theory or an ancestor of the
current theory.
\FAILURE
Fails if the named theory is not an ancestor of the current theory.
\EXAMPLE
Initially, the only parent is the main {HOL} theory:
{
#new_theory `my-theory`;;
() : void
#parents `my-theory`;;
[`HOL`] : string list
#parents `HOL`;;
[`tydefs`; `sum`; `one`; `BASIC-HOL`] : string list
#parents `tydefs`;;
[`ltree`; `BASIC-HOL`] : string list
#parents `string`;;
evaluation failed parents -- string is not an ancestor
}
\noindent However, loading the string library creates several
additional ancestor theories:
{
#load_library `string`;;
Loading library `string` ...
Updating search path
.Updating help search path
.Declaring theory string a new parent
Theory string loaded
......
Library `string` loaded.
() : void
#parents `string`;;
[`ascii`; `HOL`] : string list
#parents `my-theory`;;
[`string`; `HOL`] : string list
}
\SEEALSO
ancestors, ancestry.
\ENDDOC
|