This file is indexed.

/usr/share/hol88-2.02.19940316/Library/sets/sets.ml is in hol88-library-source 2.02.19940316-31.

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
% ===================================================================== %
% FILE		: sets.ml						%
% DESCRIPTION   : loads the library "sets" into hol.			%
%									%
% AUTHOR	: T. Melham						%
% DATE		: 90.12.01						%
% REVISED	: 91.01.23						%
% ===================================================================== %

% --------------------------------------------------------------------- %
% Put the pathname to the library sets onto the search path.		%
% --------------------------------------------------------------------- %

let path = library_pathname() ^ `/sets/` in
    tty_write `Updating search path`; 
    set_search_path (union (search_path()) [path]);;

% --------------------------------------------------------------------- %
% Add the help files to online help.					%
% --------------------------------------------------------------------- %

let path = library_pathname() ^ `/sets/help/entries/` in
    print_newline();
    tty_write `Updating help search path`; 
    set_help_search_path (union [path] (help_search_path()));;

% --------------------------------------------------------------------- %
% Load (or attempt to load) the theory sets				%
% --------------------------------------------------------------------- %

if draft_mode() 
   then (print_newline();
         print_string `Declaring theory sets a new parent`;
         print_newline();
         new_parent `sets`)
   else (print_newline();
         load_theory `sets` ?
         (tty_write `Defining ML function load_sets`;
          loadf `load_sets`;
          print_newline()));;

% --------------------------------------------------------------------- %
% Activate parser/pretty-printer support for sets (if possible).	%
% --------------------------------------------------------------------- %

if (draft_mode() or (current_theory() = `sets`)) then
   (define_set_abstraction_syntax `GSPEC`;
    define_finite_set_syntax(`EMPTY`,`INSERT`);
    set_flag(`print_set`,true); ());;

% --------------------------------------------------------------------- %
% Load compiled code if possible					%
% --------------------------------------------------------------------- %

if (draft_mode() or (current_theory() = `sets`)) then
   let path st = library_pathname() ^ `/sets/` ^ st in
       load(path `gspec`, get_flag_value `print_lib`);
       load(path `set_ind`, get_flag_value `print_lib`);
       load(path `fset_conv`, get_flag_value `print_lib`);;

% --------------------------------------------------------------------- %
% Set up autoloading of definitions and theorems from sets.th		%
% --------------------------------------------------------------------- %

if (draft_mode() or (current_theory() = `sets`)) then
   let defs = map fst (definitions `sets`) in
       map (\name. autoload_theory(`definition`,`sets`,name)) defs;
   let thms = map fst (theorems `sets`) in
       map (\name. autoload_theory(`theorem`,`sets`,name)) thms; 
   delete_cache `sets`; ();;