/usr/share/hol88-2.02.19940316/theories/one.th 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 | (SETQ %THEORYDATA (QUOTE ((PARENTS BASIC-HOL) (TYPES (0 . |one|)) (NAMETYPES) (OPERATORS (|one| |one|)) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502547926))))
(SETQ %THEOREMS (QUOTE ((SHARETYPES 4 (|fn%3| |fun| (|one|) (%VARTYPE . *)) (|f%2| |fun| (%VARTYPE . *) (|one|)) (|arb%1| %VARTYPE . *) (|rep%0| |fun| (|one|) (|bool|))) (AXIOM (|one_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |one|)) COMB ((CONST @) ABS ((VAR |x| |one|) CONST T)) |one|))) (|one_TY_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST ?) ABS ((VAR |rep| %T . |rep%0|) COMB ((COMB ((CONST TYPE_DEFINITION) ABS ((VAR |b| |bool|) VAR |b| |bool|))) VAR |rep| %T . |rep%0|) |bool|))))) (FACT (|one_Axiom| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |e| %T . |arb%1|) COMB ((CONST ?!) ABS ((VAR |fn| %T . |fn%3|) COMB ((COMB ((CONST =) COMB ((VAR |fn| %T . |fn%3|) CONST |one|))) VAR |e| %T . |arb%1|) |bool|)) |bool|)) |bool|) (|one| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |v| |one|) COMB ((COMB ((CONST =) VAR |v| |one|)) CONST |one|) |bool|)) |bool|) (|one_axiom| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%2|) COMB ((CONST !) ABS ((VAR |g| %T . |f%2|) COMB ((COMB ((CONST =) VAR |f| %T . |f%2|)) VAR |g| %T . |f%2|) |bool|)) |bool|)) |bool|) (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |arb%1|) |bool|)))))
|