HOL.Thm

data Thm

assume

axiomOfChoice

axiomOfExtensionality

axiomOfInfinity

betaConv

concl

deductAntisym

defineConst

defineTypeOp

dest

eqMp

hyp

mkAbs

mkAbsUnsafe

mkApp

mkAppUnsafe

nullHyp

refl

standardAxioms

subst