/usr/share/hol88-2.02.19940316/Library/arith/arith.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 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 | % ===================================================================== %
% FILE : arith.ml %
% DESCRIPTION : loads the library "arith" into hol. %
% %
% AUTHOR : R.J.Boulton %
% DATE : 2nd October 1992 %
% ===================================================================== %
% --------------------------------------------------------------------- %
% Load the reduce library to evaluate the formula once it has been %
% instantiated with a witness. %
% --------------------------------------------------------------------- %
load_library `reduce`;;
% --------------------------------------------------------------------- %
% Add the arith help files to online help. %
% --------------------------------------------------------------------- %
let path = library_pathname() ^ `/arith/help/entries/` in
print_string `Updating help search path`; print_newline();
set_help_search_path (union [path] (help_search_path()));;
% --------------------------------------------------------------------- %
% Begin a section for the arithmetic proof procedure code. %
% --------------------------------------------------------------------- %
begin_section arith;;
% --------------------------------------------------------------------- %
% Load the code into ml. %
% --------------------------------------------------------------------- %
let path st = library_pathname() ^ `/arith/` ^ st
and flag = get_flag_value `print_lib`
in map (\st. load(path st, flag))
[`int_extra`;
`arith_cons`;
`string_extra`;
`term_coeffs`;
`qconv`;
`decls`;
`norm_bool`;
`norm_arith`;
`norm_ineqs`;
`solve_ineqs`;
`solve`;
`rationals`;
`sup-inf`;
`streams`;
`sol_ranges`;
`exists_arith`;
`sub_and_cond`;
`prenex`;
`instance`;
`gen_arith`;
`theorems`;
`thm_convs`];;
% --------------------------------------------------------------------- %
% Export top-level functions from the section. %
% --------------------------------------------------------------------- %
(FORALL_ARITH_CONV,
EXISTS_ARITH_CONV,
SUB_AND_COND_ELIM_CONV,
COND_ELIM_CONV,
is_prenex,
PRENEX_CONV,
INSTANCE_T_CONV,
non_presburger_subterms,
is_presburger,
ARITH_CONV,
NEGATE_CONV,
(\tm. QCONV ARITH_FORM_NORM_QCONV tm ? failwith `ARITH_FORM_NORM_CONV`),
(\tm. QCONV DISJ_INEQS_FALSE_QCONV tm ? failwith `DISJ_INEQS_FALSE_CONV`)
);;
% --------------------------------------------------------------------- %
% End the section. %
% --------------------------------------------------------------------- %
end_section arith;;
% --------------------------------------------------------------------- %
% Bind the top-level functions. %
% --------------------------------------------------------------------- %
let (FORALL_ARITH_CONV,EXISTS_ARITH_CONV,
SUB_AND_COND_ELIM_CONV,COND_ELIM_CONV,is_prenex,PRENEX_CONV,
INSTANCE_T_CONV,non_presburger_subterms,is_presburger,ARITH_CONV,
NEGATE_CONV,ARITH_FORM_NORM_CONV,DISJ_INEQS_FALSE_CONV) = it;;
|