/usr/share/hol88-2.02.19940316/ml/hol-in-out.ml is in hol88-source 2.02.19940316-28.
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 | %=============================================================================%
% HOL 88 Version 2.0 %
% %
% FILE NAME: hol-in-out.ml %
% %
% DESCRIPTION: Loads in the HOL parser and printer %
% %
% USES FILES: basic-hol lisp files %
% %
% University of Cambridge %
% Hardware Verification Group %
% Computer Laboratory %
% New Museums Site %
% Pembroke Street %
% Cambridge CB2 3QG %
% England %
% %
% COPYRIGHT: University of Edinburgh %
% COPYRIGHT: University of Cambridge %
% COPYRIGHT: INRIA %
% %
% REVISION HISTORY: pathnames -- J. Joyce (April 1987) %
%=============================================================================%
% Modification J.Joyce Apr 87 %
% lisp `(setdebug t)`;; %
lisp (concat (concat `(load "` lisp_dir_pathname) `genfns")`);;
lisp (concat (concat `(load "` lisp_dir_pathname) `gnt")`);;
lisp (concat (concat `(load "` lisp_dir_pathname) `hol-pars")`);;
lisp (concat (concat `(load "` lisp_dir_pathname) `parslist")`);;
lisp (concat (concat `(load "` lisp_dir_pathname) `parslet")`);;
lisp (concat (concat `(load "` lisp_dir_pathname) `constp")`);;
lisp (concat (concat `(load "` lisp_dir_pathname) `hol-writ")`);;
lisp (concat (concat `(load "` lisp_dir_pathname) `mk_pp_thm")`);;
loadf (concat ml_dir_pathname `genfns`);; %general purpose functions%
loadf (concat ml_dir_pathname `hol-syn`);; %basic syntax functions for HOL%
|