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 | _ |
T (theorems)
TARSKI_THEOREMTC_CASES_L
TC_CASES_R
TC_CLOSED
TC_IDEMP
TC_INC
TC_INDUCT_L
TC_INDUCT_R
TC_INV
TC_MONO
TC_RC
TC_REFL
TC_RELPOW
TC_RTC_CASES_L
TC_RTC_CASES_R
TC_RTC_TC_CASES
TC_SC
TC_SYM
TC_TC_RTC_CASES
TC_TRANS
TC_TRANS_L
TC_TRANS_R
TERM
TERM1
TERMSUBST_EQ
TERMSUBST_FVT
TERMSUBST_TERMSUBST
TERMSUBST_TRIV
TERMSUBST_TWICE
TERMSUBST_TWICE_GENERAL
TERMVAL_NUMERAL
TERMVAL_TERMSUBST
TERMVAL_VALMOD_OTHER
TERMVAL_VALUATION
TERM_LEMMA1
TERM_LEMMA2
TERM_THM
THEOREMS_TRUE
TRANS_ALT
TRUE_CLOSURE
TRUE_GENERALIZE
term_CASES
term_INDUCT,term_RECURSION
termsubst
termval
th
th0
true_def