/usr/share/hol88-2.02.19940316/Library/trs/trs.ml is in hol88-library-source 2.02.19940316-19.
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 59 60 61 62 63 64 65 66 67 68 69 70 | %============================================================================%
% %
% %
% A T H E O R E M R E T R I E V A L S Y S T E M %
% %
% F O R T H E %
% %
% H O L S Y S T E M %
% %
% %
% (c) R.J.Boulton 1990 %
% %
%----------------------------------------------------------------------------%
% %
% Filename: trs.ml %
% Version: 1.0 %
% Author: Richard J. Boulton %
% Date: 14th July 1990 %
% %
% Special instructions: none %
% %
%----------------------------------------------------------------------------%
% %
% Load sub-files in the following order: %
% %
% extents.ml %
% sets.ml %
% extract.ml %
% struct.ml %
% name.ml %
% thmkind.ml %
% matching.ml %
% sidecond.ml %
% search.ml %
% user.ml %
% %
%----------------------------------------------------------------------------%
% %
% Changes history: none %
% %
%============================================================================%
% --------------------------------------------------------------------- %
% Add the trs help files to online help. %
% --------------------------------------------------------------------- %
let path1 = library_pathname() ^ `/trs/help/entries/`
and path2 = library_pathname() ^ `/trs/help/internals/`
in print_string `Updating help search path`; print_newline();
set_help_search_path (union [path1;path2] (help_search_path()));;
% --------------------------------------------------------------------- %
% Load the compiled code into ml. %
% --------------------------------------------------------------------- %
let path st = library_pathname() ^ `/trs/` ^ st
and flag = get_flag_value `print_lib`
in map (\st. load(path st, flag))
[`extents`;
`sets`;
`extract`;
`struct`;
`name`;
`thmkind`;
`matching`;
`sidecond`;
`search`;
`user`];;
%----------------------------------------------------------------------------%
|