This file is indexed.

/usr/share/hol88-2.02.19940316/Library/reduce/reduce.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
71
%******************************************************************************
** LIBRARY:     reduce (part III)                                            **
**                                                                           **
** DESCRIPTION: Reduction tools using all the conversions in the library     **
**                                                                           **
** AUTHOR:      John Harrison                                                **
**              University of Cambridge Computer Laboratory                  **
**              New Museums Site                                             **
**              Pembroke Street                                              **
**              Cambridge CB2 3QG                                            **
**              England.                                                     **
**                                                                           **
**              jrh@cl.cam.ac.uk                                             **
**                                                                           **
** DATE:        18th May 1991                                                **
** REVISED:      8th July 1991                                               **
******************************************************************************%

%-----------------------------%
% Extend the help search path %
%-----------------------------%

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

%------------------------------%
% Load the boolean conversions %
%------------------------------%

tty_write `\
Loading boolean conversions`;
load (library_pathname()^`/reduce/boolconv`,get_flag_value `print_lib`);;

%---------------------------------%
% Load the arithmetic conversions %
%---------------------------------%

tty_write `\
Loading arithmetic conversions`;
load (library_pathname()^`/reduce/arithconv`,get_flag_value `print_lib`);;

tty_write `\
Loading general conversions, rule and tactic`;;

%-----------------------------------------------------------------------%
% RED_CONV - Try all the conversions in the library                     %
%-----------------------------------------------------------------------%

let RED_CONV =
  let FAIL_CONV (s:string) (tm:term) = (failwith s) :thm in
  itlist $ORELSEC
         [ADD_CONV;  AND_CONV;  BEQ_CONV;  COND_CONV;
          DIV_CONV;  EXP_CONV;   GE_CONV;    GT_CONV;
          IMP_CONV;   LE_CONV;   LT_CONV;   MOD_CONV;
          MUL_CONV;  NEQ_CONV;  NOT_CONV;    OR_CONV;
          PRE_CONV;  SBC_CONV;  SUC_CONV] (FAIL_CONV `RED_CONV`);;

%-----------------------------------------------------------------------%
% REDUCE_CONV - Perform above reductions at any depth.                  %
%-----------------------------------------------------------------------%

let REDUCE_CONV = DEPTH_CONV RED_CONV;;

%-----------------------------------------------------------------------%
% REDUCE_RULE and REDUCE_TAC - Inference rule and tactic versions.      %
%-----------------------------------------------------------------------%

let REDUCE_RULE = CONV_RULE REDUCE_CONV;;

let REDUCE_TAC = CONV_TAC REDUCE_CONV;;