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 | _ |
D (theorems)
DEDUCTIONDEDUCTION_LEMMA
DEFINABLE_BY_ONEVAR
DEFINABLE_DEFINABLE_BY
DEFINABLE_ONEVAR
DELTA
DIFF_LEMMA
DIFF_SQUARE
DISTINCT_PRIME_COPRIME
DIVIDES_0
DIVIDES_1
DIVIDES_2
DIVIDES_ADD
DIVIDES_ADD_REVL
DIVIDES_ADD_REVR
DIVIDES_ANTISYM
DIVIDES_CASES
DIVIDES_CMUL2
DIVIDES_DIV
DIVIDES_DIVIDES_DIV
DIVIDES_DIV_MULT
DIVIDES_DIV_NOT
DIVIDES_EXP
DIVIDES_EXP2
DIVIDES_EXP_LE
DIVIDES_EXP_MINUS1
DIVIDES_EXP_PLUS1
DIVIDES_FACT
DIVIDES_FACT_PRIME
DIVIDES_GCD
DIVIDES_LE
DIVIDES_LE_STRONG
DIVIDES_LMUL
DIVIDES_LMUL2
DIVIDES_LMUL2_EQ
DIVIDES_MOD
DIVIDES_MUL2
DIVIDES_MUL_L
DIVIDES_MUL_R
DIVIDES_ONE
DIVIDES_PRIMEPOW
DIVIDES_PRIME_EXP_LE
DIVIDES_PRIME_PRIME
DIVIDES_REFL
DIVIDES_REXP
DIVIDES_REXP_SUC
DIVIDES_RMUL
DIVIDES_RMUL2
DIVIDES_RMUL2_EQ
DIVIDES_SUB
DIVIDES_TRANS
DIVIDES_TRIVIAL_UPPERBOUND
DIVIDES_ZERO
definable
definable_by
denumber
diagonalize
divides
divides_DELTA
dth