/usr/share/hol88-2.02.19940316/contrib/Predicate/predicate.ml is in hol88-contrib-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 | let pred_path = library_pathname() ^ `/predicate/` in
let sets_path = library_pathname() ^ `/sets/` in
set_search_path (union (search_path()) [pred_path; sets_path]);
print_string `(1) search path updated`; print_newline();;
if draft_mode()
then new_parent `predicate` else load_theory `predicate`;;
if draft_mode()
then (print_string `(2) predicate declared as new parent` ;
print_newline())
else (if ((current_theory() = `predicate`))
then (print_string `(2) theory predicate loaded` ;
print_newline())
else (print_string `Fail to load theory predicate!!` ;
print_newline())) ;;
associate_restriction (`!!`,`RES_qAND`) ;;
associate_restriction (`??`,`RES_qOR`) ;;
new_special_symbol `|==` ;;
load_library `taut` ;;
loadf `my_misc` ;;
if (draft_mode() or (current_theory() = `predicate`))
then load(`predicate_SUP`, get_flag_value `print_lib`) ;;
if (draft_mode() or (current_theory() = `predicate`)) then
let defs = map fst (definitions `predicate`) in
map (\name. autoload_theory(`definition`,`predicate`,name)) defs;
let thms = map fst (theorems `predicate`) in
map (\name. autoload_theory(`theorem`,`predicate`,name)) thms;
delete_cache `predicate`; ();;
|