HOL.Const
name
prov
mkUndef
isUndef
class HasConsts a
eqName
eq
selectName
select
primitives
condName
conjName
disjName
existsName
existsUniqueName
forallName
impName
negName
appendName
consName
pairName
composeName
funpowName
addName
bit0Name
bit1Name
divName
geName
gtName
leName
ltName
modName
multName
powerName
subName
zeroName
addRealName
divRealName
fromNaturalRealName
geRealName
gtRealName
leRealName
ltRealName
multRealName
powerRealName
subRealName
crossName
deleteName
differenceName
fromPredicateName
insertName
intersectName
memberName
properSubsetName
subsetName
unionName