/usr/share/hol88-2.02.19940316/contrib/SECD/hol-init.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 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 | set_search_path
(`` .
`./TACTICS/` .
`./buses/` .
`./wordn/` .
(library_pathname() ^ `/integer/`) .
(library_pathname() ^ `/group/`) .
(tl (search_path())));;
map loadf [ `load_all`
; `SYM`];;
%-----------------------------------------------------------------------
| Some useful abbreviations of rules, tactics and conversions.
------------------------------------------------------------------------%
let in_conv = DEPTH_CONV o CHANGED_CONV
and re_conv = REDEPTH_CONV o CHANGED_CONV
and in1_conv = ONCE_DEPTH_CONV
and in_conv_tac = CONV_TAC o DEPTH_CONV o CHANGED_CONV
and re_conv_tac = CONV_TAC o REDEPTH_CONV o CHANGED_CONV
and in1_conv_tac = CONV_TAC o ONCE_DEPTH_CONV
and in_conv_rule = CONV_RULE o DEPTH_CONV o CHANGED_CONV
and re_conv_rule = CONV_RULE o REDEPTH_CONV o CHANGED_CONV
and in1_conv_rule = CONV_RULE o ONCE_DEPTH_CONV
;;
let port = PURE_ONCE_REWRITE_TAC
and prt = PURE_REWRITE_TAC
and ort = ONCE_REWRITE_TAC
and rt = REWRITE_TAC
and poart = PURE_ONCE_ASM_REWRITE_TAC
and part = PURE_ASM_REWRITE_TAC
and oart = ONCE_ASM_REWRITE_TAC
and art = ASM_REWRITE_TAC
;;
let rr = REWRITE_RULE
and prr = PURE_REWRITE_RULE
and orr = ONCE_REWRITE_RULE
and porr = PURE_ONCE_REWRITE_RULE
;;
let port1 th = port[th]
and prt1 th = prt[th]
and porr1 th = porr[th]
and prr1 th = prr[th]
and poarr = PURE_ONCE_ASM_REWRITE_RULE
and parr = PURE_ASM_REWRITE_RULE
and oarr = ONCE_ASM_REWRITE_RULE
and arr = ASM_REWRITE_RULE
;;
let poke rule = POP_ASSUM \th. ASSUME_TAC (rule th);;
letrec trash n = (n = 0) => ALL_TAC | (POP_ASSUM (K ALL_TAC) THEN (trash (n-1)));;
% ================================================================= %
letrec IMP_RES_n_THEN n (ttac:thm_tactic) thm =
(n = 0) => ttac thm
| (TRY o (IMP_RES_THEN (IMP_RES_n_THEN (n - 1) ttac))) thm;;
% ================================================================= %
|