HOL.Term
dest
mk
mkConst
destConst
isConst
destGivenConst
isGivenConst
mkVar
destVar
isVar
eqVar
mkApp
mkAppUnsafe
destApp
isApp
rator
rand
land
listMkApp
listMkAppUnsafe
stripApp
mkAbs
destAbs
isAbs
listMkAbs
stripAbs
size
typeOf
isBool
sameType
sameTypeVar
alphaCompare
alphaEqual
mkEqConst
destEqConst
isEqConst
mkEq
mkEqUnsafe
destEq
isEq
lhs
rhs
rhsUnsafe
mkRefl
destRefl
isRefl
mkSelectConst
destSelectConst
isSelectConst
mkSelect
destSelect
isSelect