HOL html
| Files Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Theorems Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
I (theorems)
INDUCT_COPRIMEINDUCT_COPRIME_STRONG
IND_EUCLID
INV
ISAFFORM
ISAFTERM
icongruence
icongruence_general
icongruence_var
iff_def
iff_imp1
iff_imp2
imp_add_assum
imp_add_concl
imp_antisym
imp_contr
imp_contrf
imp_false_rule
imp_insert
imp_mono_th
imp_refl
imp_swap
imp_swap_th
imp_trans
imp_trans2
imp_trans_chain_2
imp_trans_th
imp_true_rule
imp_truefalse
imp_unduplicate
isafform
isafterm
isagform
isagterm
isaprove
ispec
ispec_lemma
isubst
isubst_general
isubst_var