/usr/share/hol88-2.02.19940316/contrib/Z/patch.ml is in hol88-contrib-source 2.02.19940316-35.
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 | %****************************************************************************%
% Patch to correct a bug in preterm handling in Common Lisp versions of %
% HOL88.2.01 %
%****************************************************************************%
if version() < 202
then (print_newline();
print_string `-------------------------------------------------------`;
print_newline();
lisp `(load '|lisp/f-gp|)`;
print_string `Version 2.02 f-gp loaded to fix preterm_handler bug`;
print_newline();
lisp `(load '|lisp/f-parser|)`;
print_string `Version 2.02 f-parser loaded to fix preterm_handler bug`;
print_newline();
lisp `(load '|lisp/f-parsml|)`;
print_string `Version 2.02 f-parsml loaded to fix preterm_handler bug`;
print_newline();
lisp `(load '|lisp/hol-pars|)`;
print_string `Version 2.02 hol-pars loaded to fix preterm_handler bug`;
print_newline();
print_string `-------------------------------------------------------`;
print_newline());;
|