hol88-help (2.02.19940316dfsg-9)
2 versions available in kali/kali-last-snapshot/main/i386
Details
Core information at a glance
- Distribution
- kali
- Origin
- kali-last-snapshot
- Repository
- https://http.kali.org/kali
- Codename
- kali-last-snapshot
- Component
- main
- Source
- hol88
- Architecture
- i386
- Section
- math
- Priority
- optional
- Maintainer
- Camm Maguire <[email protected]>
Size & integrity
Byte sizes and integrity verification
- Installed size
- 1.9 kB
- Size expected
- 209.2 kB
- Size actual
- 209.2 kB
- Size match
Dependencies
Required package dependencies
- None
Suggested packages
Recommended additional packages
- None
Description
Higher Order Logic, online help files
Tags
Package classification tags
role::documentation
Checksums
Hash values and integrity verification status
| Type | Actual | Match |
|---|---|---|
| MD5 | e218a11d…8caef0ac | |
| SHA-1 | 029a3218…99c5ba02 | |
| SHA-256 | c0033cd2…401e39bf | |
| SHA-512 | 618c6ed0…ab2c12c8 |
Contents
Files and directories included
. usr usr/share usr/share/doc usr/share/doc/hol88-help usr/share/doc/hol88-help/changelog.Debian.gz usr/share/doc/hol88-help/copyright usr/share/hol88-2.02.19940316dfsg usr/share/hol88-2.02.19940316dfsg/help usr/share/hol88-2.02.19940316dfsg/help/ENTRIES usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/#.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/*.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/+.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/-.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/..doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/.div.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/.hat.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/<.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/<<.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/=.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/>.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/@.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ABS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ABS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ACCEPT_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/AC_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ADD_ASSUM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ADD_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ALL_EL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ALL_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ALL_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ALPHA.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ALPHA_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/AND_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/AND_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ANTE_CONJ_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ANTE_RES_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/APPEND_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/AP_TERM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/AP_TERM_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/AP_THM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/AP_THM_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ASM_CASES_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ASM_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ASM_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ASSUME.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ASSUME_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ASSUM_LIST.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/B.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/BETA_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/BETA_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/BETA_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/BODY_CONJUNCTS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/BOOL_CASES_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/BUTFIRSTN_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/BUTLASTN_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/BUTLAST_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/C.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CASES_THENL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CB.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CCONTR.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CHANGED_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CHANGED_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CHECK_ASSUME_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CHOOSE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CHOOSE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CHOOSE_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/COND_CASES_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/COND_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJ.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJUNCT1.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJUNCT2.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJUNCTS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJUNCTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJUNCTS_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJUNCTS_THEN2.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJ_DISCH.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJ_DISCHL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJ_LIST.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJ_PAIR.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJ_SET_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONJ_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONTR.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONTRAPOS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONTRAPOS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONTR_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONV_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/CONV_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/Co.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DEF_EXISTS_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DEPTH_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISCARD_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISCH.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISCH_ALL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISCH_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISCH_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ1.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ1_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ2.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ2_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ_CASES.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ_CASES_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ_CASES_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ_CASES_THEN2.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ_CASES_THENL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ_CASES_UNION.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/DISJ_IMP.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ELL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQF_ELIM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQF_INTRO.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQT_ELIM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQT_INTRO.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQ_IMP_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQ_LENGTH_INDUCT_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQ_LENGTH_SNOC_INDUCT_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQ_MP.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EQ_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ETA_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EVERY.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EVERY_ASSUM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EVERY_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EVERY_TCL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTENCE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_AND_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_GREATEST_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_IMP.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_IMP_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_LEAST_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_NOT_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_OR_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXISTS_UNIQUE_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/EXT.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FAIL_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_ASM_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_ASM_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_DISCH_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_DISCH_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_GEN_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_ONCE_ASM_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_ONCE_ASM_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_PURE_ASM_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_PURE_ASM_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_PURE_ONCE_ASM_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_PURE_ONCE_ASM_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_STRIP_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FILTER_STRIP_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FIRST.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FIRSTN_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FIRST_ASSUM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FIRST_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FIRST_TCL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FLAT_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FOLDL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FOLDR_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FORALL_AND_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FORALL_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FORALL_IMP_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FORALL_NOT_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FORALL_OR_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FREEZE_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FRONT_CONJ_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/FUN_EQ_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GENL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GEN_ALL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GEN_ALPHA_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GEN_BETA_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GEN_REWRITE_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GEN_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GEN_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GEN_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GSPEC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GSUBST_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/GSYM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/HALF_MK_ABS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/I.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/IMP_ANTISYM_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/IMP_CANON.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/IMP_CONJ.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/IMP_ELIM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/IMP_RES_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/IMP_RES_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/IMP_TRANS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/INDUCT.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/INDUCT_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/INDUCT_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/INST.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/INST_TYPE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/INST_TY_TERM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ISPEC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ISPECL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/IS_EL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/K.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/KI.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LASTN_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LAST_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LEFT_AND_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LEFT_AND_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LEFT_IMP_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LEFT_IMP_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LEFT_OR_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LEFT_OR_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LENGTH_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LIST_BETA_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LIST_CONJ.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LIST_INDUCT.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LIST_INDUCT_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LIST_MK_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/LIST_MP.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MAP2_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MAP_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MAP_EVERY.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MAP_FIRST.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MATCH_ACCEPT_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MATCH_MP.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MATCH_MP_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MK_ABS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MK_COMB.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MK_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ML_eval.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MP.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/MP_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NEG_DISCH.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NOT_ELIM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NOT_EQ_SYM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NOT_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NOT_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NOT_INTRO.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NOT_MP.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NO_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NO_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/NO_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ONCE_ASM_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ONCE_ASM_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ONCE_DEPTH_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ONCE_REWRITE_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ONCE_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ONCE_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ONCE_REW_DEPTH_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ORELSE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ORELSEC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ORELSE_TCL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/OR_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/OR_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PAIRED_BETA_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PAIRED_ETA_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PART_MATCH.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/POP_ASSUM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/POP_ASSUM_LIST.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PROVE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PROVE_HYP.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_ASM_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_ASM_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_ONCE_ASM_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_ONCE_ASM_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_ONCE_REWRITE_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_ONCE_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_ONCE_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_REWRITE_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/PURE_REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RAND_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RATOR_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REDEPTH_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REFL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REFL_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REPEAT.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REPEATC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REPEAT_GTCL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REPEAT_TCL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RES_CANON.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RES_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RES_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REVERSE_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REWRITE_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REWRITE_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REWRITE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REWR_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/REW_DEPTH_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_AND_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_AND_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_BETA.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_CONV_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_IMP_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_IMP_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_LIST_BETA.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_OR_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RIGHT_OR_FORALL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RULE_ASSUM_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/RecordStep.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/S.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SCANL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SCANR_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SEG_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SELECT_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SELECT_ELIM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SELECT_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SELECT_INTRO.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SELECT_RULE.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SKOLEM_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SNOC_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SNOC_INDUCT_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SOME_EL_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SPEC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SPECL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SPEC_ALL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SPEC_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SPEC_VAR.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/STRIP_ASSUME_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/STRIP_GOAL_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/STRIP_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/STRIP_THM_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/STRUCT_CASES_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBGOAL_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBST.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBST1_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBST_ALL_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBST_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBST_MATCH.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBST_OCCS_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBST_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUBS_OCCS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SUB_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SWAP_EXISTS_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SYM.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/SYM_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/TAC_PROOF.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/THENC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/THENL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/THEN_TCL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/TOP_DEPTH_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/TRANS.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/TRY.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/TRY_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/UNDISCH.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/UNDISCH_ALL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/UNDISCH_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/VALID.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/W.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/X_CASES_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/X_CASES_THENL.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/X_CHOOSE_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/X_CHOOSE_THEN.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/X_FUN_EQ_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/X_GEN_TAC.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/X_SKOLEM_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/abs_goals.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/achieve_first.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/achieves.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/aconv.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/activate_binders.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/allowed_constant.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ancestors.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ancestry.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/append.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/append_openw.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/apply_proof.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/arb_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/arity.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ascii.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ascii_code.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/assert.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/assignable_print_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/assoc.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/associate_restriction.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/attempt_first.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/autoload.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/autoload_theory.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/axiom.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/axiom_lfn.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/axiom_msg_lfn.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/axioms.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/b.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/backup.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/backup_limit.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/backup_list.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/basic_rewrites.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/binders.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/bndvar.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/body.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/bool_EQ_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/bool_ty.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/butlast.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/cached_theories.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/can.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/change_state.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/check_lhs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/check_specification.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/check_valid.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/check_varstruct.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/chktac.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/chop_list.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/close.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/close_theory.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/com.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/combine.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/compile.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/compilef.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/compilet.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/compiling.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/compiling_stack.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/concat.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/concatl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/concl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/conjuncts.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/constants.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/current_theory.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/curry.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/define_finite_set_syntax.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/define_load_lib_function.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/define_new_type_bijections.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/define_set_abstraction_syntax.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/define_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/definition_lfn.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/definition_msg_lfn.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/definitions.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/delete_cache.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/delete_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_abs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_comb.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_cond.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_conj.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_cons.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_const.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_disj.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_eq.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_exists.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_forall.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_form.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_imp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_let.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_list.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_neg.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_neg_imp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_pabs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_pair.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_pred.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_select.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_var.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dest_vartype.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/disch.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/disjuncts.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/distinct.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/do.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/draft_mode.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/dropout.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/e.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/el.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/end_itlist.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/enter_form_rep.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/enter_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/enter_term_rep.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/exists.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/expand.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/expandf.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/explode.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/extend_theory.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/falsity.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/fast_arith.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/filter.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/find.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/find_file.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/find_match.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/find_ml_file.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/find_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/find_terms.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/find_theory.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/flags.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/flat.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/forall.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/free_in.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/frees.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/freesl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/fst.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/funpow.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/g.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/genvar.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/get_const_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/get_flag_value.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/get_state.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/get_steps.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/get_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/getenv.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/goals.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/hd.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/help.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/help_search_path.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/hide_constant.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/hol_pathname.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/host_name.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/hyp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/hyp_union.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/implode.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/infix_variable.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/infixes.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/inject_input.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/inl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/inr.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/inst.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/inst_check.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/inst_rename_list.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/inst_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/install.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/int_of_string.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/int_of_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/interface_map.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/intersect.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_abs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_alphanum.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_axiom.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_binder.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_binder_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_comb.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_cond.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_conj.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_cons.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_const.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_constant.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_disj.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_eq.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_exists.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_forall.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_hidden.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_imp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_infix.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_infix_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_let.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_letter.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_list.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_ml_curried_infix.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_ml_infix.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_ml_paired_infix.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_neg.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_neg_imp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_pabs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_pair.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_pred.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_recording_proof.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_select.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_var.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/is_vartype.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/isl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/it.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/itlist.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/itlist2.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/last.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/length.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/let_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/let_after.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/let_before.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/lhs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/libraries.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/library_loader.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/library_pathname.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/library_search_path.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/link.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/lisp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/lisp_dir_pathname.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_EQ_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_FOLD_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_mk_abs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_mk_comb.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_mk_conj.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_mk_disj.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_mk_exists.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_mk_forall.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_mk_imp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_mk_pair.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/list_of_binders.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load_axiom.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load_axioms.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load_definitions.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load_library.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load_theorem.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load_theorems.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/load_theory.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/loadf.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/loadt.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/lookup_form_rep.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/lookup_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/lookup_term_rep.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/lsp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/map.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/map2.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mapfilter.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/maptok.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/match.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/max_print_depth.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mem.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/merge_nets_rep.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/merge_term_nets.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/message.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_abs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_comb.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_cond.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_conj.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_cons.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_const.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_conv_net.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_disj.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_eq.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_exists.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_forall.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_form.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_imp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_let.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_list.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_neg.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_pabs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_pair.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_pp_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_pred.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_primed_var.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_select.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_var.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/mk_vartype.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ml_curried_infix.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ml_dir_pathname.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/ml_paired_infix.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/n_strip_quant.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_alphanum.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_axiom.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_binder.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_binder_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_constant.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_flag.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_gen_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_infix.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_infix_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_infix_list_rec_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_infix_prim_rec_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_letter.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_list_rec_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_open_axiom.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_parent.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_predicate.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_prim_rec_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_recursive_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_special_symbol.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_specification.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_stack.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_syntax_block.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_theory.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_type_abbrev.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/new_type_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/nil_term_net.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/not.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/null.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/num_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/num_EQ_CONV.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/o.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/oo.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/openi.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/openw.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/outl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/outr.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/p.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/pair.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/paired_delete_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/paired_new_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/paired_theorem.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/parents.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/parse_as_binder.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/partition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/pop_proofs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/pop_proofs_print.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/pp_axiom.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/preterm_abs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/preterm_antiquot.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/preterm_comb.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/preterm_const.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/preterm_to_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/preterm_typed.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/preterm_var.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_all_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_begin.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_bool.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_break.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_defined_types.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_end.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_goal.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_hyps.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_ibegin.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_int.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_list.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_newline.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_stack.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_state.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_string.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_subgoals.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_theory.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_tok.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_unquoted_term.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_unquoted_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/print_void.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prompt.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_abs_fn_one_one.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_abs_fn_onto.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_cases_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_constructors_distinct.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_constructors_one_one.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_induction_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_rec_fn_exists.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_rep_fn_one_one.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_rep_fn_onto.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/prove_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/push_fsubgoals.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/push_print.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/push_subgoals.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/quit.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/r.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rand.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rator.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/read.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/record_proof.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/remove.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/remove_sticky_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rep_goals.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/replicate.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/resume_recording.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rev.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rev_assoc.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rev_itlist.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rhs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/root_goal.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rotate.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rotate_goals.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/rotate_top.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/save.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/save_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/save_top_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/search_path.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_equal.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_fail.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_fail_prefix.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_flag.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_goal.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_help.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_help_search_path.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_interface_map.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_lambda.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_library_search_path.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_margin.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_pretty_mode.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_prompt.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_search_path.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_state.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_sticky_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_string_escape.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_thm_count.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/set_turnstile.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/setify.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/show_types.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/snd.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/sort.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/special_symbols.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/split.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/splitp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/sticky_list.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/store_binders.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/store_definition.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/string_of_int.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/strip_abs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/strip_comb.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/strip_exists.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/strip_forall.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/strip_imp.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/strip_pair.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/subst.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/subst_occs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/subtract.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/suspend_recording.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/syserror.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/system.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/term_of_int.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/theorem.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/theorem_lfn.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/theorem_msg_lfn.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/theorems.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/thm_count.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/thm_frees.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/timer.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/tl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/top_goal.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/top_print.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/top_proof.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/top_thm.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/tryfind.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/tty_read.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/tty_write.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/type_abbrevs.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/type_in.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/type_in_type.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/type_of.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/type_tyvars.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/types.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/tyvars.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/tyvarsl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/uncurry.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/undo_autoload.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/unhide_constant.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/union.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/unlink.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/variant.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/vars.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/varsl.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/version.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/word_separators.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/words.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/words2.doc usr/share/hol88-2.02.19940316dfsg/help/ENTRIES/write.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_ASSOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_CLAUSES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_EQ_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_EQ_SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_INV_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_INV_0_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_MONO_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ADD_SYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ASSOC_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ASSOC_MULT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/CANCEL_SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/DA.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/DIVISION.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/DIV_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/DIV_MULT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/DIV_UNIQUE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EQ_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EQ_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EQ_MONO_ADD_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN_AND_ODD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN_DOUBLE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN_MULT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN_ODD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN_ODD_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EVEN_OR_ODD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EXP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/EXP_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/FACT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/FACT_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/FUN_EQ_LEMMA.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/GREATER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/GREATER_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/GREATER_OR_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/INDUCTION.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/INV_PRE_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/INV_PRE_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/INV_PRE_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/INV_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/INV_SUC_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/IS_NUM_REP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LEFT_ADD_DISTRIB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LEFT_ID_ADD_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LEFT_ID_MULT_1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LEFT_SUB_DISTRIB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_0_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_0_CASES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_ADD_1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_ADD_NONZERO.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_ADD_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_ANTISYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_CASES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_CASES_IMP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQUAL_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQUAL_ANTISYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_ADD_SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_ANTISYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_CASES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_IMP_LESS_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_LESS_EQ_MONO.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_LESS_TRANS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_MONO.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_MONO_ADD_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_REFL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_SUB_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_SUC_REFL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EQ_TRANS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_EXP_SUC_MONO.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_IMP_LESS_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_IMP_LESS_OR_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_LEMMA1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_LEMMA2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_LESS_CASES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_LESS_EQ_TRANS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_LESS_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MOD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MONO.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MONO_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MONO_ADD_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MONO_ADD_INV.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MONO_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MONO_MULT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MONO_REV.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MULT2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_MULT_MONO.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_NOT_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_NOT_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_OR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_OR_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_OR_EQ_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_REFL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_SUB_ADD_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_SUC_EQ_COR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_SUC_IMP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_SUC_NOT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_SUC_REFL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_SUC_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/LESS_TRANS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MOD_EQ_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MOD_MOD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MOD_MULT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MOD_ONE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MOD_PLUS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MOD_TIMES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MOD_UNIQUE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MONOID_ADD_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MONOID_MULT_1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_ASSOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_CLAUSES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_EQ_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_EXP_MONO.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_LEFT_1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_LESS_EQ_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_MONO_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_RIGHT_1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_SUC_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/MULT_SYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_EXP_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_GREATER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_GREATER_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_LEQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_LESS_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_LESS_EQUAL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_NUM_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_ODD_EQ_EVEN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_SUC_ADD_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_SUC_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/NOT_SUC_LESS_EQ_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ODD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ODD_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ODD_DOUBLE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ODD_EVEN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ODD_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ODD_MULT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ODD_OR_EVEN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/OR_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRE_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRE_SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRE_SUB1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRE_SUC_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRIM_REC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRIM_REC_EQN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRIM_REC_FUN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/PRIM_REC_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/RIGHT_ADD_DISTRIB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/RIGHT_ID_ADD_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/RIGHT_ID_MULT_1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/RIGHT_SUB_DISTRIB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SIMP_REC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SIMP_REC_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SIMP_REC_FUN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SIMP_REC_FUN_LEMMA.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SIMP_REC_REL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SIMP_REC_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_CANCEL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_EQUAL_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_EQ_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_EQ_EQ_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LEFT_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LEFT_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LEFT_GREATER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LEFT_GREATER_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LEFT_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LEFT_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LEFT_SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LEFT_SUC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LESS_0.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LESS_EQ_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_LESS_OR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_MONO_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_PLUS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_RIGHT_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_RIGHT_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_RIGHT_GREATER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_RIGHT_GREATER_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_RIGHT_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_RIGHT_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_RIGHT_SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUB_SUB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUC_ADD_SYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUC_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUC_ID.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUC_LESS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUC_NOT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUC_ONE_ADD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUC_REP_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/SUC_SUB1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/TIMES2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/WOP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ZERO_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ZERO_DIV.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ZERO_LESS_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ZERO_LESS_EXP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ZERO_MOD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/ZERO_REP_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/num_Axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/num_CASES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/num_ISO_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/arith/num_TY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/axioms usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/axioms/ARB_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/axioms/BOOL_CASES_AX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/axioms/ETA_AX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/axioms/IMP_ANTISYM_AX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/axioms/INFINITY_AX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/axioms/SELECT_AX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic/AND_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic/EXISTS_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic/EXISTS_UNIQUE_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic/FORALL_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic/F_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic/NOT_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic/OR_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/basic-logic/T_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/I_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/I_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/I_o_ID.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/K_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/K_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/S_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/S_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/o_ASSOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/o_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/combin/o_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/ABS_SIMP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/ASSOC_CONJ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/ASSOC_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/ASSOC_DISJ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/COMM_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/EQ_EXT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/FCOMM_ASSOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/FCOMM_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/FUN_EQ_LEMMA.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/LEFT_ID_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/MONOID_CONJ_T.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/MONOID_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/MONOID_DISJ_F.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/ONE_ONE_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/ONTO_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/functions/RIGHT_ID_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_CONJ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_FIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_FOLDL_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_FOLDR_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_REPLICATE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ALL_EL_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/AND_EL_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/AND_EL_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/AND_EL_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/AP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_ASSOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_BUTLASTN_BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_BUTLASTN_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_BUTLAST_LAST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_FIRSTN_BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_FIRSTN_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_LENGTH_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/APPEND_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ASSOC_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ASSOC_FOLDL_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ASSOC_FOLDR_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_APPEND1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_APPEND2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_LENGTH_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_LENGTH_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTFIRSTN_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLAST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_APPEND1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_APPEND2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_BUTLAST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_FIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_LASTN_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_LENGTH_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_LENGTH_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_LENGTH_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLASTN_SUC_BUTLAST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/BUTLAST_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/COMM_ASSOC_FOLDL_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/COMM_ASSOC_FOLDR_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/COMM_MONOID_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/COMM_MONOID_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/CONS_11.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/CONS_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/CONS_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_0_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_APPEND1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_APPEND2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_IS_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_LAST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_LENGTH_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_LENGTH_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_LENGTH_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_PRE_LENGTH.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_REVERSE_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ELL_SUC_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_APPEND1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_APPEND2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_ELL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_IS_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_LENGTH_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_LENGTH_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_PRE_LENGTH.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_REVERSE_ELL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EL_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/EQ_LIST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FCOMM_FOLDL_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FCOMM_FOLDL_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FCOMM_FOLDR_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FCOMM_FOLDR_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_COMM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_FILTER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_IDEM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FILTER_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_APPEND1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_APPEND2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_FIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_LENGTH_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_LENGTH_ID.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FIRSTN_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FLAT_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FLAT_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FLAT_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FLAT_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FLAT_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FLAT_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL_FILTER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL_FOLDR_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL_SINGLE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDL_SNOC_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_CONS_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_FILTER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_FILTER_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_FOLDL_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_MAP_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_SINGLE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/FOLDR_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/GENLIST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/HD.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_FILTER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_FIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_FOLDL_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_FOLDR_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_REPLICATE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_EL_SOME_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_PREFIX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_PREFIX_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_PREFIX_IS_SUBLIST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_PREFIX_PREFIX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_PREFIX_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_SUBLIST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_SUBLIST_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_SUBLIST_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_SUFFIX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_SUFFIX_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_SUFFIX_IS_SUBLIST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_SUFFIX_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/IS_list_REP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LAST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_APPEND1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_APPEND2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_LENGTH_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_LENGTH_ID.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LASTN_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LAST_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LAST_LASTN_LAST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_BUTLAST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_EQ_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_EQ_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_FIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_GENLIST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_MAP2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_NOT_NULL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_REPLICATE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_SCANL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_SCANR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_UNZIP_FST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_UNZIP_SND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LENGTH_ZIP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/LIST_NOT_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP2_ZIP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_FILTER.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_MAP_o.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MAP_o.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/MONOID_APPEND_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NIL_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NOT_ALL_EL_SOME_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NOT_CONS_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NOT_EQ_LIST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NOT_NIL_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NOT_NIL_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NOT_SNOC_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NOT_SOME_EL_ALL_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NULL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NULL_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NULL_EQ_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NULL_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/NULL_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/OR_EL_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/OR_EL_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/OR_EL_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/PART.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/PREFIX.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/PREFIX_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/PREFIX_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REPLICATE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REVERSE_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REVERSE_EQ_NIL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REVERSE_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REVERSE_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REVERSE_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REVERSE_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/REVERSE_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SCANL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SCANR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_0_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_APPEND1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_APPEND2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_FIRSTN_BUTFISTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_LASTN_BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_LENGTH_ID.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_LENGTH_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SEG_SUC_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC_11.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC_Axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC_CASES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC_EQ_LENGTH_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC_INDUCT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SNOC_REVERSE_CONS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_BUTFIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_BUTLASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_DISJ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_FIRSTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_FOLDL_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_FOLDR_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_LASTN.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_MAP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_SEG.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SOME_EL_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SPLIT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SPLITP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SUFFIX_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SUM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SUM_APPEND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SUM_FLAT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SUM_FOLDL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SUM_FOLDR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SUM_REVERSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/SUM_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/TL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/TL_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/UNZIP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/UNZIP_FST_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/UNZIP_SND_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/UNZIP_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/UNZIP_ZIP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ZIP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ZIP_SNOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/ZIP_UNZIP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/list_Axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/list_CASES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/list_INDUCT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/list_ISO_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/list/list_TY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/AND1_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/AND2_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/AND_CLAUSES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/AND_IMP_INTRO.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/AND_INTRO_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/BOOL_EQ_DISTINCT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/COND_ABS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/COND_CLAUSES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/COND_EXPAND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/COND_ID.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/COND_RAND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/COND_RATOR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/CONJ_ASSOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/CONJ_SYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/DE_MORGAN_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/DISJ_ASSOC.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/DISJ_SYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EQ_CLAUSES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EQ_EXPAND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EQ_IMP_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EQ_REFL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EQ_SYM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EQ_SYM_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EQ_TRANS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EXCLUDED_MIDDLE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/EXISTS_SIMP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/FALSITY.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/FORALL_SIMP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/F_IMP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/IMP_CLAUSES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/IMP_DISJ_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/IMP_F.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/IMP_F_EQ_F.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/IS_ASSUMPTION_OF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/LEFT_AND_OVER_OR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/LEFT_OR_OVER_AND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/NOT_AND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/NOT_CLAUSES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/NOT_F.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/NOT_IMP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/OR_CLAUSES.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/OR_ELIM_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/OR_IMP_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/OR_INTRO_THM1.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/OR_INTRO_THM2.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/REFL_CLAUSE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/RIGHT_AND_OVER_OR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/RIGHT_OR_OVER_AND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/SELECT_REFL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/SELECT_UNIQUE.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/logic/TRUTH.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/one usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/one/one.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/one/one_Axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/one/one_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/one/one_TY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/one/one_axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/COMMA_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/CURRY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/FST.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/FST_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/IS_PAIR_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/PAIR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/PAIR_EQ.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/PAIR_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/REP_prod.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/SND.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/SND_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/UNCURRY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/pairs/prod_TY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/INL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/INL_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/INR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/INR_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/ISL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/ISL_OR_ISR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/ISR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/IS_SUM_REP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/OUTL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/OUTR.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/sum_Axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/sum_ISO_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/sum_TY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/sum/sum_axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/syntax usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/syntax/ARB.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/syntax/COND_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/syntax/LET_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/syntax/RES_ABSTRACT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/syntax/RES_EXISTS.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/syntax/RES_FORALL.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/syntax/RES_SELECT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/AP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/HT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/Is_ltree.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/Is_tree_REP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/Node.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/Node_11.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/Node_onto.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/PART.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/SPLIT.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/Size.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/bht.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/dest_node.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/ltree_Axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/ltree_ISO_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/ltree_Induct.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/ltree_TY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/node.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/node_11.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/node_REP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/tree_Axiom.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/tree_ISO_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/tree_Induct.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/tree_TY_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tree/trf.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tydefs usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tydefs/ABS_REP_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tydefs/TRP.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tydefs/TRP_DEF.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tydefs/TYPE_DEFINITION.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tydefs/TY_DEF_THM.doc usr/share/hol88-2.02.19940316dfsg/help/THEOREMS/tydefs/exists_TRP.doc usr/share/lintian usr/share/lintian/overrides usr/share/lintian/overrides/hol88-help