hol88-help 2.02.19940316-35 / usr / share / hol88-2.02.19940316 / help / THEOREMS / arith

This file is indexed.

/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ is in hol88-help 2.02.19940316-35.

This file is owned by root:root, with mode 0o755.

File Mime Type Owner Mode Size
..
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD.doc text/plain root:root 0o644 91 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD1.doc text/plain root:root 0o644 58 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_0.doc text/plain root:root 0o644 55 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_ASSOC.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_CLAUSES.doc text/plain root:root 0o644 143 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_EQ_0.doc text/plain root:root 0o644 83 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_EQ_SUB.doc text/plain root:root 0o644 93 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_INV_0.doc text/plain root:root 0o644 75 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_INV_0_EQ.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_MONO_LESS_EQ.doc text/plain root:root 0o644 88 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_SUB.doc text/plain root:root 0o644 65 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_SUC.doc text/plain root:root 0o644 74 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ADD_SYM.doc text/plain root:root 0o644 63 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ASSOC_ADD.doc text/plain root:root 0o644 54 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ASSOC_MULT.doc text/plain root:root 0o644 55 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/CANCEL_SUB.doc text/plain root:root 0o644 103 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/DA.doc text/plain root:root 0o644 89 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/DIVISION.doc text/plain root:root 0o644 119 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/DIV_LESS_EQ.doc text/plain root:root 0o644 82 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/DIV_MULT.doc text/plain root:root 0o644 90 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/DIV_UNIQUE.doc text/plain root:root 0o644 105 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EQ_LESS.doc text/plain root:root 0o644 67 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EQ_LESS_EQ.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EQ_MONO_ADD_EQ.doc text/plain root:root 0o644 84 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN.doc text/plain root:root 0o644 84 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN_ADD.doc text/plain root:root 0o644 82 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN_AND_ODD.doc text/plain root:root 0o644 71 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN_DOUBLE.doc text/plain root:root 0o644 63 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN_EXISTS.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN_MULT.doc text/plain root:root 0o644 82 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN_ODD.doc text/plain root:root 0o644 64 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN_ODD_EXISTS.doc text/plain root:root 0o644 120 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EVEN_OR_ODD.doc text/plain root:root 0o644 67 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EXP.doc text/plain root:root 0o644 98 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/EXP_ADD.doc text/plain root:root 0o644 89 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/FACT.doc text/plain root:root 0o644 95 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/FACT_LESS.doc text/plain root:root 0o644 62 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/FUN_EQ_LEMMA.doc text/plain root:root 0o644 87 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/GREATER.doc text/plain root:root 0o644 63 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/GREATER_EQ.doc text/plain root:root 0o644 68 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/GREATER_OR_EQ.doc text/plain root:root 0o644 81 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/INDUCTION.doc text/plain root:root 0o644 86 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/INV_PRE_EQ.doc text/plain root:root 0o644 99 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/INV_PRE_LESS.doc text/plain root:root 0o644 94 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/INV_PRE_LESS_EQ.doc text/plain root:root 0o644 99 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/INV_SUC.doc text/plain root:root 0o644 70 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/INV_SUC_EQ.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/IS_NUM_REP.doc text/plain root:root 0o644 121 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LEFT_ADD_DISTRIB.doc text/plain root:root 0o644 92 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LEFT_ID_ADD_0.doc text/plain root:root 0o644 62 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LEFT_ID_MULT_1.doc text/plain root:root 0o644 63 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LEFT_SUB_DISTRIB.doc text/plain root:root 0o644 92 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS.doc text/plain root:root 0o644 99 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_0.doc text/plain root:root 0o644 56 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_0_0.doc text/plain root:root 0o644 54 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_0_CASES.doc text/plain root:root 0o644 69 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_ADD.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_ADD_1.doc text/plain root:root 0o644 84 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_ADD_NONZERO.doc text/plain root:root 0o644 83 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_ADD_SUC.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_ANTISYM.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_CASES.doc text/plain root:root 0o644 68 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_CASES_IMP.doc text/plain root:root 0o644 85 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ.doc text/plain root:root 0o644 70 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQUAL_ADD.doc text/plain root:root 0o644 83 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQUAL_ANTISYM.doc text/plain root:root 0o644 89 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_0.doc text/plain root:root 0o644 66 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_ADD.doc text/plain root:root 0o644 66 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_ADD_SUB.doc text/plain root:root 0o644 100 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_ANTISYM.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_CASES.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_EXISTS.doc text/plain root:root 0o644 81 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_IMP_LESS_SUC.doc text/plain root:root 0o644 85 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_LESS_EQ_MONO.doc text/plain root:root 0o644 106 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_LESS_TRANS.doc text/plain root:root 0o644 88 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_MONO.doc text/plain root:root 0o644 82 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_MONO_ADD_EQ.doc text/plain root:root 0o644 91 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_REFL.doc text/plain root:root 0o644 59 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_SUB_LESS.doc text/plain root:root 0o644 101 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_SUC_REFL.doc text/plain root:root 0o644 69 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EQ_TRANS.doc text/plain root:root 0o644 85 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_EXP_SUC_MONO.doc text/plain root:root 0o644 109 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_IMP_LESS_ADD.doc text/plain root:root 0o644 87 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_IMP_LESS_OR_EQ.doc text/plain root:root 0o644 78 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_LEMMA1.doc text/plain root:root 0o644 84 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_LEMMA2.doc text/plain root:root 0o644 84 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_LESS_CASES.doc text/plain root:root 0o644 83 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_LESS_EQ_TRANS.doc text/plain root:root 0o644 88 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_LESS_SUC.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MOD.doc text/plain root:root 0o644 74 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MONO.doc text/plain root:root 0o644 77 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MONO_ADD.doc text/plain root:root 0o644 85 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MONO_ADD_EQ.doc text/plain root:root 0o644 86 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MONO_ADD_INV.doc text/plain root:root 0o644 89 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MONO_EQ.doc text/plain root:root 0o644 80 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MONO_MULT.doc text/plain root:root 0o644 88 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MONO_REV.doc text/plain root:root 0o644 83 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MULT2.doc text/plain root:root 0o644 83 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_MULT_MONO.doc text/plain root:root 0o644 96 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_NOT_EQ.doc text/plain root:root 0o644 70 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_NOT_SUC.doc text/plain root:root 0o644 92 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_OR.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_OR_EQ.doc text/plain root:root 0o644 78 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_OR_EQ_ADD.doc text/plain root:root 0o644 81 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_REFL.doc text/plain root:root 0o644 54 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_SUB_ADD_LESS.doc text/plain root:root 0o644 89 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_SUC.doc text/plain root:root 0o644 70 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_SUC_EQ_COR.doc text/plain root:root 0o644 95 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_SUC_IMP.doc text/plain root:root 0o644 87 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_SUC_NOT.doc text/plain root:root 0o644 77 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_SUC_REFL.doc text/plain root:root 0o644 63 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_SUC_SUC.doc text/plain root:root 0o644 82 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_THM.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/LESS_TRANS.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MOD_EQ_0.doc text/plain root:root 0o644 82 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MOD_MOD.doc text/plain root:root 0o644 89 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MOD_MULT.doc text/plain root:root 0o644 90 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MOD_ONE.doc text/plain root:root 0o644 65 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MOD_PLUS.doc text/plain root:root 0o644 112 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MOD_TIMES.doc text/plain root:root 0o644 97 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MOD_UNIQUE.doc text/plain root:root 0o644 105 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MONOID_ADD_0.doc text/plain root:root 0o644 60 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MONOID_MULT_1.doc text/plain root:root 0o644 61 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT.doc text/plain root:root 0o644 93 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_0.doc text/plain root:root 0o644 56 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_ASSOC.doc text/plain root:root 0o644 80 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_CLAUSES.doc text/plain root:root 0o644 197 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_EQ_0.doc text/plain root:root 0o644 84 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_EXP_MONO.doc text/plain root:root 0o644 113 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_LEFT_1.doc text/plain root:root 0o644 61 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_LESS_EQ_SUC.doc text/plain root:root 0o644 100 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_MONO_EQ.doc text/plain root:root 0o644 94 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_RIGHT_1.doc text/plain root:root 0o644 62 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_SUC.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_SUC_EQ.doc text/plain root:root 0o644 93 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/MULT_SYM.doc text/plain root:root 0o644 64 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_EXP_0.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_GREATER.doc text/plain root:root 0o644 69 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_GREATER_EQ.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_LEQ.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_LESS.doc text/plain root:root 0o644 66 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_LESS_0.doc text/plain root:root 0o644 55 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_LESS_EQ.doc text/plain root:root 0o644 70 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_LESS_EQUAL.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_NUM_EQ.doc text/plain root:root 0o644 92 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_ODD_EQ_EVEN.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_SUC.doc text/plain root:root 0o644 53 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_SUC_ADD_LESS_EQ.doc text/plain root:root 0o644 80 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_SUC_LESS_EQ.doc text/plain root:root 0o644 80 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/NOT_SUC_LESS_EQ_0.doc text/plain root:root 0o644 71 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ODD.doc text/plain root:root 0o644 80 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ODD_ADD.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ODD_DOUBLE.doc text/plain root:root 0o644 66 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ODD_EVEN.doc text/plain root:root 0o644 64 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ODD_EXISTS.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ODD_MULT.doc text/plain root:root 0o644 78 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ODD_OR_EVEN.doc text/plain root:root 0o644 110 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/OR_LESS.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRE.doc text/plain root:root 0o644 73 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRE_DEF.doc text/plain root:root 0o644 86 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRE_SUB.doc text/plain root:root 0o644 74 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRE_SUB1.doc text/plain root:root 0o644 62 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRE_SUC_EQ.doc text/plain root:root 0o644 90 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRIM_REC.doc text/plain root:root 0o644 93 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRIM_REC_EQN.doc text/plain root:root 0o644 159 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRIM_REC_FUN.doc text/plain root:root 0o644 111 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/PRIM_REC_THM.doc text/plain root:root 0o644 131 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/RIGHT_ADD_DISTRIB.doc text/plain root:root 0o644 93 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/RIGHT_ID_ADD_0.doc text/plain root:root 0o644 64 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/RIGHT_ID_MULT_1.doc text/plain root:root 0o644 65 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/RIGHT_SUB_DISTRIB.doc text/plain root:root 0o644 93 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SIMP_REC.doc text/plain root:root 0o644 92 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SIMP_REC_EXISTS.doc text/plain root:root 0o644 86 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SIMP_REC_FUN.doc text/plain root:root 0o644 106 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SIMP_REC_FUN_LEMMA.doc text/plain root:root 0o644 191 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SIMP_REC_REL.doc text/plain root:root 0o644 146 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SIMP_REC_THM.doc text/plain root:root 0o644 130 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB.doc text/plain root:root 0o644 106 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_0.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_ADD.doc text/plain root:root 0o644 78 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_CANCEL.doc text/plain root:root 0o644 103 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_EQUAL_0.doc text/plain root:root 0o644 61 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_EQ_0.doc text/plain root:root 0o644 71 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_EQ_EQ_0.doc text/plain root:root 0o644 86 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LEFT_ADD.doc text/plain root:root 0o644 98 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LEFT_EQ.doc text/plain root:root 0o644 101 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LEFT_GREATER.doc text/plain root:root 0o644 95 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LEFT_GREATER_EQ.doc text/plain root:root 0o644 91 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LEFT_LESS.doc text/plain root:root 0o644 83 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LEFT_LESS_EQ.doc text/plain root:root 0o644 98 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LEFT_SUB.doc text/plain root:root 0o644 98 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LEFT_SUC.doc text/plain root:root 0o644 99 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LESS_0.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LESS_EQ.doc text/plain root:root 0o644 66 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LESS_EQ_ADD.doc text/plain root:root 0o644 102 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_LESS_OR.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_MONO_EQ.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_PLUS.doc text/plain root:root 0o644 78 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_RIGHT_ADD.doc text/plain root:root 0o644 99 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_RIGHT_EQ.doc text/plain root:root 0o644 102 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_RIGHT_GREATER.doc text/plain root:root 0o644 87 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_RIGHT_GREATER_EQ.doc text/plain root:root 0o644 102 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_RIGHT_LESS.doc text/plain root:root 0o644 93 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_RIGHT_LESS_EQ.doc text/plain root:root 0o644 89 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_RIGHT_SUB.doc text/plain root:root 0o644 83 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUB_SUB.doc text/plain root:root 0o644 92 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUC_ADD_SYM.doc text/plain root:root 0o644 78 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUC_DEF.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUC_ID.doc text/plain root:root 0o644 57 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUC_LESS.doc text/plain root:root 0o644 70 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUC_NOT.doc text/plain root:root 0o644 60 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUC_ONE_ADD.doc text/plain root:root 0o644 65 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUC_REP_DEF.doc text/plain root:root 0o644 77 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/SUC_SUB1.doc text/plain root:root 0o644 64 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/TIMES2.doc text/plain root:root 0o644 60 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/WOP.doc text/plain root:root 0o644 91 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ZERO_DEF.doc text/plain root:root 0o644 58 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ZERO_DIV.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ZERO_LESS_EQ.doc text/plain root:root 0o644 59 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ZERO_LESS_EXP.doc text/plain root:root 0o644 75 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ZERO_MOD.doc text/plain root:root 0o644 72 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/ZERO_REP_DEF.doc text/plain root:root 0o644 79 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/num_Axiom.doc text/plain root:root 0o644 97 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/num_CASES.doc text/plain root:root 0o644 76 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/num_ISO_DEF.doc text/plain root:root 0o644 121 bytes
/usr/share/hol88-2.02.19940316/help/THEOREMS/arith/num_TY_DEF.doc text/plain root:root 0o644 76 bytes

APT Browse - Built by Thomas Orozco.