/usr/share/hol88-2.02.19940316/contrib/convert/convert.ml is in hol88-contrib-source 2.02.19940316-14.
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 | % ===================================================================== %
% FILE : convert.ml %
% DESCRIPTION : loads the library "convert" into hol. %
% %
% AUTHOR : D Shepherd %
% REVISED : 90.12.01 (TFM). %
% ===================================================================== %
%< =====================================================================
convert library
contents:
conv_package.ml: conversion package
unfold.ml: unfolding rules
unwind.ml: unwinding rules
prune.ml: pruning rules
more_conv.ml: some extra conversions
The unfolding and unwinding comes from original HOL sources.
The pruning conversions have been rewritten to be tidier and
more theoretically sound (i.e. no mk_thms)
conv_package was inspired by interface to occam transformation system
and allows detailed term hacking in a (semi-)controlled environemnt.
more_conv contains some extra conversions and conversionals.
david shepherd <des@inmos.co.uk>
===================================================================== >%
% --------------------------------------------------------------------- %
% Load the compiled code into ml. %
% --------------------------------------------------------------------- %
let path st = library_pathname() ^ `/convert/` ^ st in
load(path `conv_package`, get_flag_value `print_lib`);
load(path `unfold`, get_flag_value `print_lib`);
load(path `unwind`, get_flag_value `print_lib`);
load(path `prune`, get_flag_value `print_lib`);
load(path `more_conv`, get_flag_value `print_lib`);;
|