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 | _ |
A (theorems)
ADD_IMP_SUBADD_SUM_DIFF
ALLN
ARITH_DIAGONALIZE
ARITH_GNUMERAL
ARITH_GNUMERAL1
ARITH_GNUMERAL1'
ARITH_PAIR
ARITH_PRIMREC
ARITH_PRIMRECSTEP
ARITH_PROV
ARITH_PROV1
ARITH_QDIAG
ASSIGN
ASSIGN_TRIV
AXIOM
AXIOMS_TRUE
AXIOM_FORMULA
AXIOM_THM
AXIOM_THM_STRONG
add_assum
alpha
arith_gnumeral
arith_gnumeral1
arith_gnumeral1'
arith_pair
arith_primrec
arith_primrecstep
arith_prov
arith_qdiag
assign
assume
axiom_addimp
axiom_allimp
axiom_and
axiom_distribimp
axiom_doubleneg
axiom_eqrefl
axiom_exists
axiom_existseq
axiom_funcong
axiom_iffimp1
axiom_iffimp2
axiom_impall
axiom_impiff
axiom_not
axiom_or
axiom_predcong
axiom_true