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 | _ |
S (theorems)
SC_CLOSEDSC_EXPLICIT
SC_IDEMP
SC_INC
SC_INV
SC_INV_STRONG
SC_MONO
SC_RC
SC_REFL
SC_SYM
SC_TC
SEMCOMPLETE_IMP_COMPLETE
SEMCOMPLETE_SOUND_EQ_CONSISTENT
SETMAX
SETMAX_LEMMA
SETMAX_MEMBER
SETMAX_THM
SETMAX_UNION
SIGMA
SIGMAPI_AXIOM
SIGMAPI_CLAUSES
SIGMAPI_CLAUSES_CODE
SIGMAPI_DIAGONALIZE
SIGMAPI_DIVIDES
SIGMAPI_FIXPOINT
SIGMAPI_FORM
SIGMAPI_FORM1
SIGMAPI_FORMSUBST
SIGMAPI_FREEFORM
SIGMAPI_FREEFORM1
SIGMAPI_FREETERM
SIGMAPI_FREETERM1
SIGMAPI_GNUMERAL
SIGMAPI_GNUMERAL1
SIGMAPI_GSENTENCE
SIGMAPI_HSENTENCE
SIGMAPI_MONO_LEMMA
SIGMAPI_PRIME
SIGMAPI_PRIMEPOW
SIGMAPI_PRIMREC
SIGMAPI_PRIMRECSTEP
SIGMAPI_PROP
SIGMAPI_PROV
SIGMAPI_PROV1
SIGMAPI_QDIAG
SIGMAPI_QSUBST
SIGMAPI_REV_EXISTS
SIGMAPI_REV_FORALL
SIGMAPI_RTC
SIGMAPI_RTCP
SIGMAPI_TERM
SIGMAPI_TERM1
SOUND_CLOSED
SOUND_IMP_CONSISTENT
STC
STC_CASES
STC_CASES_L
STC_CASES_R
STC_CLOSED
STC_IDEMP
STC_INC
STC_INC_SC
STC_INC_TC
STC_INDUCT
STC_INV
STC_MONO
STC_REFL
STC_SYM
STC_TRANS
STC_TRANS_L
STC_TRANS_R
SYM_ALT
semcomplete
sound
sound_for
spec
subalpha
subspec