hol-1.4: Higher order logic

Index

absHOL.Conv
AbsConstProvHOL.Data
AbsTermHOL.Data
AbsTermCommandHOL.OpenTheory.Article
AbsThmCommandHOL.OpenTheory.Article
addNameHOL.Const
addRealNameHOL.Const
addRequiresHOL.OpenTheory.Package
advanceParseIntegerHOL.Parse
alpha 
1 (Function)HOL.TypeVar
2 (Function)HOL.Type
3 (Function)HOL.Rule
alphaCompareHOL.Term
alphaEqualHOL.Term
alphaHypHOL.Rule
alphaSequentHOL.Rule
appendInfoHOL.OpenTheory.Package
appendNameHOL.Const
applyHOL.Conv
applyDataHOL.Conv
applyTermHOL.Conv
AppTermHOL.Data
AppTermCommandHOL.OpenTheory.Article
AppThmCommandHOL.OpenTheory.Article
ArticleHOL.OpenTheory.Package
AssocHOL.Print
assumeHOL.Thm
AssumeCommandHOL.OpenTheory.Article
avoidCaptureHOL.Subst
AxiomCommandHOL.OpenTheory.Article
axiomOfChoice 
1 (Function)HOL.TermAlpha
2 (Function)HOL.Sequent
3 (Function)HOL.Thm
axiomOfExtensionality 
1 (Function)HOL.TermAlpha
2 (Function)HOL.Sequent
3 (Function)HOL.Thm
axiomOfInfinity 
1 (Function)HOL.TermAlpha
2 (Function)HOL.Sequent
3 (Function)HOL.Thm
basicSubst 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
beta 
1 (Function)HOL.TypeVar
2 (Function)HOL.Type
3 (Function)HOL.Conv
betaConvHOL.Thm
BetaConvCommandHOL.OpenTheory.Article
betaSimpHOL.Conv
bit0NameHOL.Const
bit1NameHOL.Const
Block 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
blockHOL.OpenTheory.Package
Blocks 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
bool 
1 (Function)HOL.TypeOp
2 (Function)HOL.Type
boolNameHOL.TypeOp
boolNamespaceHOL.Name
bottomUpHOL.Conv
CanSubst 
1 (Type/Class)HOL.TypeSubst
2 (Type/Class)HOL.Subst
capturableVarsHOL.Subst
ChangedHOL.Conv
checksumHOL.OpenTheory.Package
closedHOL.Var
CommandHOL.OpenTheory.Article
compose 
1 (Function)HOL.TypeSubst
2 (Function)HOL.OpenTheory.Interpret
composeNameHOL.Const
concatInfoHOL.OpenTheory.Package
concatRenamesHOL.OpenTheory.Interpret
concl 
1 (Function)HOL.Sequent
2 (Function)HOL.Thm
condHOL.Conv
condNameHOL.Const
conjNameHOL.Const
ConsCommandHOL.OpenTheory.Article
consNameHOL.Const
Const 
1 (Type/Class)HOL.Data
2 (Data Constructor)HOL.Data
ConstCommandHOL.OpenTheory.Article
ConstDef 
1 (Type/Class)HOL.Data
2 (Data Constructor)HOL.Data
constMapHOL.Theory
ConstObjectHOL.OpenTheory.Article
ConstProvHOL.Data
constsHOL.Const
ConstSymbolHOL.OpenTheory.Interpret
ConstTermHOL.Data
ConstTermCommandHOL.OpenTheory.Article
Conv 
1 (Type/Class)HOL.Conv
2 (Data Constructor)HOL.Conv
crossNameHOL.Const
dataSubst 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
deductAntisymHOL.Thm
DeductAntisymCommandHOL.OpenTheory.Article
DefCommandHOL.OpenTheory.Article
DefConstProvHOL.Data
defineConstHOL.Thm
DefineConstCommandHOL.OpenTheory.Article
defineConstListHOL.Rule
DefineConstListCommandHOL.OpenTheory.Article
defineTypeOpHOL.Thm
DefineTypeOpCommandHOL.OpenTheory.Article
defineTypeOpLegacyHOL.Rule
DefineTypeOpLegacyCommandHOL.OpenTheory.Article
defStateHOL.OpenTheory.Article
DefTypeOpProvHOL.Data
deleteNameHOL.Const
dest 
1 (Function)HOL.TypeVar
2 (Function)HOL.Type
3 (Function)HOL.TypeSubst
4 (Function)HOL.Var
5 (Function)HOL.Term
6 (Function)HOL.Subst
7 (Function)HOL.TermAlpha
8 (Function)HOL.Sequent
9 (Function)HOL.Thm
destAbs 
1 (Function)HOL.TermData
2 (Function)HOL.Term
destApp 
1 (Function)HOL.TermData
2 (Function)HOL.Term
destBinaryOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
destBlockHOL.OpenTheory.Package
destBlocksHOL.OpenTheory.Package
destConst 
1 (Function)HOL.TermData
2 (Function)HOL.Term
destEq 
1 (Function)HOL.Type
2 (Function)HOL.Term
destEqConstHOL.Term
destFileHOL.OpenTheory.Package
destFunHOL.Type
destGivenConst 
1 (Function)HOL.TermData
2 (Function)HOL.Term
destGivenOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
destGlobalHOL.Name
destInfoHOL.OpenTheory.Package
destNameHOL.OpenTheory.Package
destOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
destPredHOL.Type
destReflHOL.Term
destRelHOL.Type
destRenameHOL.OpenTheory.Interpret
destRenamesHOL.OpenTheory.Interpret
destSelect 
1 (Function)HOL.Type
2 (Function)HOL.Term
destSelectConstHOL.Term
destUnaryOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
destVar 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
3 (Function)HOL.TermData
4 (Function)HOL.Term
destVersionHOL.OpenTheory.Package
dictHOL.OpenTheory.Article
differenceNameHOL.Const
directoryHOL.OpenTheory.Package
directoryVersionHOL.OpenTheory.Package
disjNameHOL.Const
divNameHOL.Const
divRealNameHOL.Const
domainHOL.Type
empty 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
3 (Function)HOL.Theory
4 (Function)HOL.OpenTheory.Interpret
emptyRequiresHOL.OpenTheory.Package
endParseIntegerHOL.Parse
eolParserHOL.Parse
eqHOL.Const
eqMpHOL.Thm
EqMpCommandHOL.OpenTheory.Article
eqName 
1 (Function)HOL.Const
2 (Function)HOL.TypeVar
eqVar 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
3 (Function)HOL.TermData
4 (Function)HOL.Term
ErrorParseIntegerHOL.Parse
evalHOL.Conv
executeCommandHOL.OpenTheory.Article
existsNameHOL.Const
existsUniqueNameHOL.Const
failHOL.Conv
File 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
firstGetInfoHOL.OpenTheory.Package
firstInfoHOL.OpenTheory.Package
FoldlParseIntegerHOL.Parse
forallNameHOL.Const
freeHOL.Var
freeInHOL.Var
freeInMultiple 
1 (Function)HOL.TermData
2 (Function)HOL.Term
freeInOnceHOL.Term
freshSupplyHOL.Name
fromInfoHOL.OpenTheory.Package
fromList 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
fromListRequiresHOL.OpenTheory.Package
fromListUnsafeHOL.Subst
fromNaturalRealNameHOL.Const
fromObjectHOL.OpenTheory.Article
fromPredicateNameHOL.Const
fromRenamesHOL.OpenTheory.Interpret
fromRenamesUnsafeHOL.OpenTheory.Interpret
fromStringHOL.Parse
fromStringUnsafeHOL.Parse
fromTextHOL.Parse
fromTextFileHOL.Parse
fromThmSetHOL.Theory
funHOL.TypeOp
functionNamespaceHOL.Name
funNameHOL.TypeOp
funpowNameHOL.Const
geNameHOL.Const
geRealNameHOL.Const
getInfoHOL.OpenTheory.Package
globalHOL.Name
gtNameHOL.Const
gtRealNameHOL.Const
HasConstsHOL.Const
HasFreeHOL.Var
HasOpsHOL.TypeOp
HasVarsHOL.TypeVar
HdTlCommandHOL.OpenTheory.Article
hyp 
1 (Function)HOL.Sequent
2 (Function)HOL.Thm
idHOL.Conv
impNameHOL.Const
importsHOL.OpenTheory.Package
IncludeHOL.OpenTheory.Package
ind 
1 (Function)HOL.TypeOp
2 (Function)HOL.Type
indNameHOL.TypeOp
InfixOpHOL.Print
Info 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
informationHOL.OpenTheory.Package
InformativeHOL.OpenTheory.Package
initialStateHOL.OpenTheory.Article
insertNameHOL.Const
Interpret 
1 (Type/Class)HOL.OpenTheory.Interpret
2 (Data Constructor)HOL.OpenTheory.Interpret
3 (Data Constructor)HOL.OpenTheory.Package
interpret 
1 (Function)HOL.OpenTheory.Interpret
2 (Function)HOL.OpenTheory.Package
Interpretation 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
interpretConstHOL.OpenTheory.Interpret
interpretTypeOpHOL.OpenTheory.Interpret
intersectNameHOL.Const
isAbs 
1 (Function)HOL.TermData
2 (Function)HOL.Term
isApp 
1 (Function)HOL.TermData
2 (Function)HOL.Term
isBinaryOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
isBool 
1 (Function)HOL.Type
2 (Function)HOL.Term
3 (Function)HOL.TermAlpha
isConst 
1 (Function)HOL.TermData
2 (Function)HOL.Term
isEq 
1 (Function)HOL.Type
2 (Function)HOL.Term
isEqConstHOL.Term
isFunHOL.Type
isGivenConst 
1 (Function)HOL.TermData
2 (Function)HOL.Term
isGivenOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
isGlobalHOL.Name
isIndHOL.Type
isNullaryOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
isOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
isPredHOL.Type
isReflHOL.Term
isRelHOL.Type
isSelect 
1 (Function)HOL.Type
2 (Function)HOL.Term
isSelectConstHOL.Term
isSymbolCharHOL.Print
isSymbolStringHOL.Print
isUnaryOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
isUndef 
1 (Function)HOL.Const
2 (Function)HOL.TypeOp
isVar 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
3 (Function)HOL.TermData
4 (Function)HOL.Term
KeyValue 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
landHOL.Term
LeftAssocHOL.Print
leNameHOL.Const
leRealNameHOL.Const
lhsHOL.Term
LineNumberHOL.OpenTheory.Article
lineParserHOL.Parse
listGetInfoHOL.OpenTheory.Package
listMkAbsHOL.Term
listMkAppHOL.Term
listMkAppUnsafeHOL.Term
listMkFunHOL.Type
listNamespaceHOL.Name
ListObjectHOL.OpenTheory.Article
lookupConstHOL.Theory
lookupConstUnsafeHOL.Theory
lookupThmHOL.Theory
lookupTypeOpHOL.Theory
lookupTypeOpUnsafeHOL.Theory
ltNameHOL.Const
ltRealNameHOL.Const
mapGetInfoHOL.OpenTheory.Package
matchKeyValueHOL.OpenTheory.Package
maybeGetInfoHOL.OpenTheory.Package
memberNameHOL.Const
mk 
1 (Function)HOL.TypeVar
2 (Function)HOL.Type
3 (Function)HOL.TypeSubst
4 (Function)HOL.Var
5 (Function)HOL.Term
6 (Function)HOL.Subst
7 (Function)HOL.TermAlpha
8 (Function)HOL.Sequent
9 (Function)HOL.OpenTheory.Interpret
mkAbs 
1 (Function)HOL.TermData
2 (Function)HOL.Term
3 (Function)HOL.Thm
mkAbsUnsafeHOL.Thm
mkApp 
1 (Function)HOL.TermData
2 (Function)HOL.Term
3 (Function)HOL.Thm
mkAppUnsafe 
1 (Function)HOL.Term
2 (Function)HOL.Thm
mkBlockHOL.OpenTheory.Package
mkBlocksHOL.OpenTheory.Package
mkConst 
1 (Function)HOL.TermData
2 (Function)HOL.Term
mkEq 
1 (Function)HOL.Type
2 (Function)HOL.Term
mkEqConstHOL.Term
mkEqUnsafeHOL.Term
mkFunHOL.Type
mkGlobalHOL.Name
mkNullHypHOL.Sequent
mkNullHypUnsafeHOL.Sequent
mkOp 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
mkPredHOL.Type
mkReflHOL.Term
mkRelHOL.Type
mkSelect 
1 (Function)HOL.Type
2 (Function)HOL.Term
mkSelectConstHOL.Term
mkUndef 
1 (Function)HOL.Const
2 (Function)HOL.TypeOp
mkUnsafe 
1 (Function)HOL.Util
2 (Function)HOL.Subst
3 (Function)HOL.Sequent
mkUnsafe1HOL.Util
mkUnsafe2HOL.Util
mkVar 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
3 (Function)HOL.TermData
4 (Function)HOL.Term
modNameHOL.Const
multNameHOL.Const
multRealNameHOL.Const
Name 
1 (Type/Class)HOL.Name
2 (Data Constructor)HOL.Name
3 (Type/Class)HOL.OpenTheory.Package
4 (Data Constructor)HOL.OpenTheory.Package
name 
1 (Function)HOL.Const
2 (Function)HOL.TypeOp
3 (Function)HOL.Var
4 (Function)HOL.OpenTheory.Package
NameCommandHOL.OpenTheory.Article
NameObjectHOL.OpenTheory.Article
Namespace 
1 (Type/Class)HOL.Name
2 (Data Constructor)HOL.Name
NameVersion 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
naturalNameHOL.TypeOp
naturalNamespaceHOL.Name
NegativeParseIntegerHOL.Parse
negNameHOL.Const
NilCommandHOL.OpenTheory.Article
NonAssocHOL.Print
NonZeroParseIntegerHOL.Parse
notFreeInHOL.Var
null 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
nullHyp 
1 (Function)HOL.Sequent
2 (Function)HOL.Thm
nullInfoHOL.OpenTheory.Package
Number 
1 (Type/Class)HOL.OpenTheory.Article
2 (Data Constructor)HOL.OpenTheory.Article
NumberCommandHOL.OpenTheory.Article
NumberObjectHOL.OpenTheory.Article
ObjectHOL.OpenTheory.Article
ObjectiveHOL.OpenTheory.Article
opentheoryHOL.OpenTheory.Package
opentheoryDirectoryHOL.OpenTheory.Package
OperationHOL.OpenTheory.Package
operationHOL.OpenTheory.Package
opsHOL.TypeOp
OpTypeHOL.Data
OpTypeCommandHOL.OpenTheory.Article
orelseHOL.Conv
Package 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
packageHOL.OpenTheory.Package
packageFileHOL.OpenTheory.Package
pairNameHOL.Const
pairNamespaceHOL.Name
ParsableHOL.Parse
ParseIntegerHOL.Parse
parseIntegerHOL.Parse
parseKeyValueHOL.OpenTheory.Package
parserHOL.Parse
peekStateHOL.OpenTheory.Article
pop2ObjectHOL.OpenTheory.Article
pop2StateHOL.OpenTheory.Article
pop3ObjectHOL.OpenTheory.Article
pop3StateHOL.OpenTheory.Article
pop4ObjectHOL.OpenTheory.Article
pop5ObjectHOL.OpenTheory.Article
pop5StateHOL.OpenTheory.Article
PopCommandHOL.OpenTheory.Article
popObjectHOL.OpenTheory.Article
popStateHOL.OpenTheory.Article
powerNameHOL.Const
powerRealNameHOL.Const
ppInfixOpsHOL.Print
ppPrefixOpsHOL.Print
ppSymbolNameHOL.Print
PragmaCommandHOL.OpenTheory.Article
PrecHOL.Print
PrefixOpHOL.Print
primitives 
1 (Function)HOL.Const
2 (Function)HOL.TypeOp
PrintableHOL.Print
printKeyValueHOL.OpenTheory.Package
productNameHOL.TypeOp
properSubsetNameHOL.Const
prov 
1 (Function)HOL.Const
2 (Function)HOL.TypeOp
proveHypHOL.Rule
ProveHypCommandHOL.OpenTheory.Article
push2ObjectHOL.OpenTheory.Article
push2StateHOL.OpenTheory.Article
push3ObjectHOL.OpenTheory.Article
push4ObjectHOL.OpenTheory.Article
push5ObjectHOL.OpenTheory.Article
push5StateHOL.OpenTheory.Article
pushObjectHOL.OpenTheory.Article
pushStateHOL.OpenTheory.Article
quoteNameHOL.Print
quoteNamespaceHOL.Print
rand 
1 (Function)HOL.Term
2 (Function)HOL.Rule
3 (Function)HOL.Conv
randUnsafeHOL.Rule
rangeHOL.Type
rator 
1 (Function)HOL.Term
2 (Function)HOL.Rule
3 (Function)HOL.Conv
ratorUnsafeHOL.Rule
readArticle 
1 (Function)HOL.OpenTheory.Article
2 (Function)HOL.OpenTheory
readBlockHOL.OpenTheory.Package
readBlocksHOL.OpenTheory.Package
readInterpretationHOL.OpenTheory.Package
readListHOL.OpenTheory.Package
readPackageHOL.OpenTheory.Package
readPackageFileHOL.OpenTheory.Package
readPackagesHOL.OpenTheory
readVersionHOL.OpenTheory.Package
realNamespaceHOL.Name
RefCommandHOL.OpenTheory.Article
reflHOL.Thm
ReflCommandHOL.OpenTheory.Article
refStateHOL.OpenTheory.Article
regularCommandsHOL.OpenTheory.Article
RemoveCommandHOL.OpenTheory.Article
removeStateHOL.OpenTheory.Article
Rename 
1 (Type/Class)HOL.OpenTheory.Interpret
2 (Data Constructor)HOL.OpenTheory.Interpret
renameAvoidingHOL.Var
renameBoundVarHOL.Subst
renameFreshHOL.Term
Renames 
1 (Type/Class)HOL.OpenTheory.Interpret
2 (Data Constructor)HOL.OpenTheory.Interpret
renameSymbolHOL.OpenTheory.Interpret
RepConstProvHOL.Data
repeatHOL.Conv
Requires 
1 (Type/Class)HOL.OpenTheory.Package
2 (Data Constructor)HOL.OpenTheory.Package
requiresHOL.OpenTheory.Package
ResultHOL.Conv
rhsHOL.Term
rhsUnsafeHOL.Term
RightAssocHOL.Print
sameTypeHOL.Term
sameTypeVarHOL.Term
selectHOL.Const
selectNameHOL.Const
Sequent 
1 (Type/Class)HOL.Sequent
2 (Data Constructor)HOL.Sequent
sequentObjectHOL.OpenTheory.Article
sequentsHOL.Theory
setNamespaceHOL.Name
sharingSubst 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
singleton 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
singletonUnsafeHOL.Subst
SizeHOL.Data
size 
1 (Function)HOL.TypeData
2 (Function)HOL.Type
3 (Function)HOL.TermData
4 (Function)HOL.Term
sourceHOL.OpenTheory.Package
spaceParserHOL.Parse
stackHOL.OpenTheory.Article
standardHOL.Theory
standardAxiomNameHOL.TermAlpha
standardAxioms 
1 (Function)HOL.TermAlpha
2 (Function)HOL.Sequent
3 (Function)HOL.Thm
StartParseIntegerHOL.Parse
State 
1 (Type/Class)HOL.OpenTheory.Article
2 (Data Constructor)HOL.OpenTheory.Article
stripAbsHOL.Term
stripAppHOL.Term
stripFunHOL.Type
subHOL.Conv
subNameHOL.Const
subRealNameHOL.Const
subsetNameHOL.Const
Subst 
1 (Type/Class)HOL.Subst
2 (Data Constructor)HOL.Subst
subst 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
3 (Function)HOL.Thm
SubstCommandHOL.OpenTheory.Article
sucNameHOL.Const
sumNameHOL.TypeOp
sumNamespaceHOL.Name
supportedCommandHOL.OpenTheory.Article
symHOL.Rule
SymbolHOL.OpenTheory.Interpret
symbolNameHOL.OpenTheory.Interpret
SymCommandHOL.OpenTheory.Article
Term 
1 (Type/Class)HOL.Data
2 (Data Constructor)HOL.Data
TermAlpha 
1 (Type/Class)HOL.TermAlpha
2 (Data Constructor)HOL.TermAlpha
TermDataHOL.Data
TermIdHOL.Data
TermObjectHOL.OpenTheory.Article
thencHOL.Conv
theoremsHOL.OpenTheory.Article
Theory 
1 (Type/Class)HOL.Theory
2 (Data Constructor)HOL.Theory
ThmHOL.Thm
ThmCommandHOL.OpenTheory.Article
thmMapHOL.Theory
ThmObjectHOL.OpenTheory.Article
thmsHOL.Theory
thmStateHOL.OpenTheory.Article
toDocHOL.Print
toInfoHOL.OpenTheory.Package
toObjectHOL.OpenTheory.Article
toRenamesHOL.OpenTheory.Interpret
toStringHOL.Print
toStringWithHOL.Print
transHOL.Rule
TransCommandHOL.OpenTheory.Article
transUnsafeHOL.Rule
tryHOL.Conv
trySharingSubst 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
trySubst 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
tryTypeSubstHOL.Subst
Type 
1 (Type/Class)HOL.Data
2 (Data Constructor)HOL.Data
TypeDataHOL.Data
TypeIdHOL.Data
TypeObjectHOL.OpenTheory.Article
typeOf 
1 (Function)HOL.Var
2 (Function)HOL.TermData
3 (Function)HOL.Term
4 (Function)HOL.TermAlpha
TypeOp 
1 (Type/Class)HOL.Data
2 (Data Constructor)HOL.Data
TypeOpCommandHOL.OpenTheory.Article
TypeOpDef 
1 (Type/Class)HOL.Data
2 (Data Constructor)HOL.Data
typeOpMapHOL.Theory
TypeOpObjectHOL.OpenTheory.Article
TypeOpProvHOL.Data
TypeOpSymbolHOL.OpenTheory.Interpret
TypeSubst 
1 (Type/Class)HOL.TypeSubst
2 (Data Constructor)HOL.TypeSubst
typeSubstHOL.Subst
TypeVar 
1 (Type/Class)HOL.Data
2 (Data Constructor)HOL.Data
UnchangedHOL.Conv
UndefConstProvHOL.Data
UndefTypeOpProvHOL.Data
UnionHOL.OpenTheory.Package
unionHOL.Theory
unionListHOL.Theory
unionNameHOL.Const
Var 
1 (Type/Class)HOL.Data
2 (Data Constructor)HOL.Data
VarCommandHOL.OpenTheory.Article
variantAvoidingHOL.Name
VarObjectHOL.OpenTheory.Article
varsHOL.TypeVar
varSubst 
1 (Function)HOL.TypeSubst
2 (Function)HOL.Subst
VarTermHOL.Data
VarTermCommandHOL.OpenTheory.Article
VarTypeHOL.Data
VarTypeCommandHOL.OpenTheory.Article
Version 
1 (Type/Class)HOL.OpenTheory.Article
2 (Type/Class)HOL.OpenTheory.Package
3 (Data Constructor)HOL.OpenTheory.Package
versionHOL.OpenTheory.Package
VersionCommandHOL.OpenTheory.Article
versionCommandHOL.OpenTheory.Article
zeroNameHOL.Const
ZeroParseIntegerHOL.Parse