hol-1.4: Higher order logic
Contents
Index
Index
abs
HOL.Conv
AbsConstProv
HOL.Data
AbsTerm
HOL.Data
AbsTermCommand
HOL.OpenTheory.Article
AbsThmCommand
HOL.OpenTheory.Article
addName
HOL.Const
addRealName
HOL.Const
addRequires
HOL.OpenTheory.Package
advanceParseInteger
HOL.Parse
alpha
1 (Function)
HOL.TypeVar
2 (Function)
HOL.Type
3 (Function)
HOL.Rule
alphaCompare
HOL.Term
alphaEqual
HOL.Term
alphaHyp
HOL.Rule
alphaSequent
HOL.Rule
appendInfo
HOL.OpenTheory.Package
appendName
HOL.Const
apply
HOL.Conv
applyData
HOL.Conv
applyTerm
HOL.Conv
AppTerm
HOL.Data
AppTermCommand
HOL.OpenTheory.Article
AppThmCommand
HOL.OpenTheory.Article
Article
HOL.OpenTheory.Package
Assoc
HOL.Print
assume
HOL.Thm
AssumeCommand
HOL.OpenTheory.Article
avoidCapture
HOL.Subst
AxiomCommand
HOL.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
betaConv
HOL.Thm
BetaConvCommand
HOL.OpenTheory.Article
betaSimp
HOL.Conv
bit0Name
HOL.Const
bit1Name
HOL.Const
Block
1 (Type/Class)
HOL.OpenTheory.Package
2 (Data Constructor)
HOL.OpenTheory.Package
block
HOL.OpenTheory.Package
Blocks
1 (Type/Class)
HOL.OpenTheory.Package
2 (Data Constructor)
HOL.OpenTheory.Package
bool
1 (Function)
HOL.TypeOp
2 (Function)
HOL.Type
boolName
HOL.TypeOp
boolNamespace
HOL.Name
bottomUp
HOL.Conv
CanSubst
1 (Type/Class)
HOL.TypeSubst
2 (Type/Class)
HOL.Subst
capturableVars
HOL.Subst
Changed
HOL.Conv
checksum
HOL.OpenTheory.Package
closed
HOL.Var
Command
HOL.OpenTheory.Article
compose
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.OpenTheory.Interpret
composeName
HOL.Const
concatInfo
HOL.OpenTheory.Package
concatRenames
HOL.OpenTheory.Interpret
concl
1 (Function)
HOL.Sequent
2 (Function)
HOL.Thm
cond
HOL.Conv
condName
HOL.Const
conjName
HOL.Const
ConsCommand
HOL.OpenTheory.Article
consName
HOL.Const
Const
1 (Type/Class)
HOL.Data
2 (Data Constructor)
HOL.Data
ConstCommand
HOL.OpenTheory.Article
ConstDef
1 (Type/Class)
HOL.Data
2 (Data Constructor)
HOL.Data
constMap
HOL.Theory
ConstObject
HOL.OpenTheory.Article
ConstProv
HOL.Data
consts
HOL.Const
ConstSymbol
HOL.OpenTheory.Interpret
ConstTerm
HOL.Data
ConstTermCommand
HOL.OpenTheory.Article
Conv
1 (Type/Class)
HOL.Conv
2 (Data Constructor)
HOL.Conv
crossName
HOL.Const
dataSubst
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
deductAntisym
HOL.Thm
DeductAntisymCommand
HOL.OpenTheory.Article
DefCommand
HOL.OpenTheory.Article
DefConstProv
HOL.Data
defineConst
HOL.Thm
DefineConstCommand
HOL.OpenTheory.Article
defineConstList
HOL.Rule
DefineConstListCommand
HOL.OpenTheory.Article
defineTypeOp
HOL.Thm
DefineTypeOpCommand
HOL.OpenTheory.Article
defineTypeOpLegacy
HOL.Rule
DefineTypeOpLegacyCommand
HOL.OpenTheory.Article
defState
HOL.OpenTheory.Article
DefTypeOpProv
HOL.Data
deleteName
HOL.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
destBlock
HOL.OpenTheory.Package
destBlocks
HOL.OpenTheory.Package
destConst
1 (Function)
HOL.TermData
2 (Function)
HOL.Term
destEq
1 (Function)
HOL.Type
2 (Function)
HOL.Term
destEqConst
HOL.Term
destFile
HOL.OpenTheory.Package
destFun
HOL.Type
destGivenConst
1 (Function)
HOL.TermData
2 (Function)
HOL.Term
destGivenOp
1 (Function)
HOL.TypeData
2 (Function)
HOL.Type
destGlobal
HOL.Name
destInfo
HOL.OpenTheory.Package
destName
HOL.OpenTheory.Package
destOp
1 (Function)
HOL.TypeData
2 (Function)
HOL.Type
destPred
HOL.Type
destRefl
HOL.Term
destRel
HOL.Type
destRename
HOL.OpenTheory.Interpret
destRenames
HOL.OpenTheory.Interpret
destSelect
1 (Function)
HOL.Type
2 (Function)
HOL.Term
destSelectConst
HOL.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
destVersion
HOL.OpenTheory.Package
dict
HOL.OpenTheory.Article
differenceName
HOL.Const
directory
HOL.OpenTheory.Package
directoryVersion
HOL.OpenTheory.Package
disjName
HOL.Const
divName
HOL.Const
divRealName
HOL.Const
domain
HOL.Type
empty
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
3 (Function)
HOL.Theory
4 (Function)
HOL.OpenTheory.Interpret
emptyRequires
HOL.OpenTheory.Package
endParseInteger
HOL.Parse
eolParser
HOL.Parse
eq
HOL.Const
eqMp
HOL.Thm
EqMpCommand
HOL.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
ErrorParseInteger
HOL.Parse
eval
HOL.Conv
executeCommand
HOL.OpenTheory.Article
existsName
HOL.Const
existsUniqueName
HOL.Const
fail
HOL.Conv
File
1 (Type/Class)
HOL.OpenTheory.Package
2 (Data Constructor)
HOL.OpenTheory.Package
firstGetInfo
HOL.OpenTheory.Package
firstInfo
HOL.OpenTheory.Package
FoldlParseInteger
HOL.Parse
forallName
HOL.Const
free
HOL.Var
freeIn
HOL.Var
freeInMultiple
1 (Function)
HOL.TermData
2 (Function)
HOL.Term
freeInOnce
HOL.Term
freshSupply
HOL.Name
fromInfo
HOL.OpenTheory.Package
fromList
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
fromListRequires
HOL.OpenTheory.Package
fromListUnsafe
HOL.Subst
fromNaturalRealName
HOL.Const
fromObject
HOL.OpenTheory.Article
fromPredicateName
HOL.Const
fromRenames
HOL.OpenTheory.Interpret
fromRenamesUnsafe
HOL.OpenTheory.Interpret
fromString
HOL.Parse
fromStringUnsafe
HOL.Parse
fromText
HOL.Parse
fromTextFile
HOL.Parse
fromThmSet
HOL.Theory
fun
HOL.TypeOp
functionNamespace
HOL.Name
funName
HOL.TypeOp
funpowName
HOL.Const
geName
HOL.Const
geRealName
HOL.Const
getInfo
HOL.OpenTheory.Package
global
HOL.Name
gtName
HOL.Const
gtRealName
HOL.Const
HasConsts
HOL.Const
HasFree
HOL.Var
HasOps
HOL.TypeOp
HasVars
HOL.TypeVar
HdTlCommand
HOL.OpenTheory.Article
hyp
1 (Function)
HOL.Sequent
2 (Function)
HOL.Thm
id
HOL.Conv
impName
HOL.Const
imports
HOL.OpenTheory.Package
Include
HOL.OpenTheory.Package
ind
1 (Function)
HOL.TypeOp
2 (Function)
HOL.Type
indName
HOL.TypeOp
InfixOp
HOL.Print
Info
1 (Type/Class)
HOL.OpenTheory.Package
2 (Data Constructor)
HOL.OpenTheory.Package
information
HOL.OpenTheory.Package
Informative
HOL.OpenTheory.Package
initialState
HOL.OpenTheory.Article
insertName
HOL.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
interpretConst
HOL.OpenTheory.Interpret
interpretTypeOp
HOL.OpenTheory.Interpret
intersectName
HOL.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
isEqConst
HOL.Term
isFun
HOL.Type
isGivenConst
1 (Function)
HOL.TermData
2 (Function)
HOL.Term
isGivenOp
1 (Function)
HOL.TypeData
2 (Function)
HOL.Type
isGlobal
HOL.Name
isInd
HOL.Type
isNullaryOp
1 (Function)
HOL.TypeData
2 (Function)
HOL.Type
isOp
1 (Function)
HOL.TypeData
2 (Function)
HOL.Type
isPred
HOL.Type
isRefl
HOL.Term
isRel
HOL.Type
isSelect
1 (Function)
HOL.Type
2 (Function)
HOL.Term
isSelectConst
HOL.Term
isSymbolChar
HOL.Print
isSymbolString
HOL.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
land
HOL.Term
LeftAssoc
HOL.Print
leName
HOL.Const
leRealName
HOL.Const
lhs
HOL.Term
LineNumber
HOL.OpenTheory.Article
lineParser
HOL.Parse
listGetInfo
HOL.OpenTheory.Package
listMkAbs
HOL.Term
listMkApp
HOL.Term
listMkAppUnsafe
HOL.Term
listMkFun
HOL.Type
listNamespace
HOL.Name
ListObject
HOL.OpenTheory.Article
lookupConst
HOL.Theory
lookupConstUnsafe
HOL.Theory
lookupThm
HOL.Theory
lookupTypeOp
HOL.Theory
lookupTypeOpUnsafe
HOL.Theory
ltName
HOL.Const
ltRealName
HOL.Const
mapGetInfo
HOL.OpenTheory.Package
matchKeyValue
HOL.OpenTheory.Package
maybeGetInfo
HOL.OpenTheory.Package
memberName
HOL.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
mkAbsUnsafe
HOL.Thm
mkApp
1 (Function)
HOL.TermData
2 (Function)
HOL.Term
3 (Function)
HOL.Thm
mkAppUnsafe
1 (Function)
HOL.Term
2 (Function)
HOL.Thm
mkBlock
HOL.OpenTheory.Package
mkBlocks
HOL.OpenTheory.Package
mkConst
1 (Function)
HOL.TermData
2 (Function)
HOL.Term
mkEq
1 (Function)
HOL.Type
2 (Function)
HOL.Term
mkEqConst
HOL.Term
mkEqUnsafe
HOL.Term
mkFun
HOL.Type
mkGlobal
HOL.Name
mkNullHyp
HOL.Sequent
mkNullHypUnsafe
HOL.Sequent
mkOp
1 (Function)
HOL.TypeData
2 (Function)
HOL.Type
mkPred
HOL.Type
mkRefl
HOL.Term
mkRel
HOL.Type
mkSelect
1 (Function)
HOL.Type
2 (Function)
HOL.Term
mkSelectConst
HOL.Term
mkUndef
1 (Function)
HOL.Const
2 (Function)
HOL.TypeOp
mkUnsafe
1 (Function)
HOL.Util
2 (Function)
HOL.Subst
3 (Function)
HOL.Sequent
mkUnsafe1
HOL.Util
mkUnsafe2
HOL.Util
mkVar
1 (Function)
HOL.TypeData
2 (Function)
HOL.Type
3 (Function)
HOL.TermData
4 (Function)
HOL.Term
modName
HOL.Const
multName
HOL.Const
multRealName
HOL.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
NameCommand
HOL.OpenTheory.Article
NameObject
HOL.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
naturalName
HOL.TypeOp
naturalNamespace
HOL.Name
NegativeParseInteger
HOL.Parse
negName
HOL.Const
NilCommand
HOL.OpenTheory.Article
NonAssoc
HOL.Print
NonZeroParseInteger
HOL.Parse
notFreeIn
HOL.Var
null
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
nullHyp
1 (Function)
HOL.Sequent
2 (Function)
HOL.Thm
nullInfo
HOL.OpenTheory.Package
Number
1 (Type/Class)
HOL.OpenTheory.Article
2 (Data Constructor)
HOL.OpenTheory.Article
NumberCommand
HOL.OpenTheory.Article
NumberObject
HOL.OpenTheory.Article
Object
HOL.OpenTheory.Article
Objective
HOL.OpenTheory.Article
opentheory
HOL.OpenTheory.Package
opentheoryDirectory
HOL.OpenTheory.Package
Operation
HOL.OpenTheory.Package
operation
HOL.OpenTheory.Package
ops
HOL.TypeOp
OpType
HOL.Data
OpTypeCommand
HOL.OpenTheory.Article
orelse
HOL.Conv
Package
1 (Type/Class)
HOL.OpenTheory.Package
2 (Data Constructor)
HOL.OpenTheory.Package
package
HOL.OpenTheory.Package
packageFile
HOL.OpenTheory.Package
pairName
HOL.Const
pairNamespace
HOL.Name
Parsable
HOL.Parse
ParseInteger
HOL.Parse
parseInteger
HOL.Parse
parseKeyValue
HOL.OpenTheory.Package
parser
HOL.Parse
peekState
HOL.OpenTheory.Article
pop2Object
HOL.OpenTheory.Article
pop2State
HOL.OpenTheory.Article
pop3Object
HOL.OpenTheory.Article
pop3State
HOL.OpenTheory.Article
pop4Object
HOL.OpenTheory.Article
pop5Object
HOL.OpenTheory.Article
pop5State
HOL.OpenTheory.Article
PopCommand
HOL.OpenTheory.Article
popObject
HOL.OpenTheory.Article
popState
HOL.OpenTheory.Article
powerName
HOL.Const
powerRealName
HOL.Const
ppInfixOps
HOL.Print
ppPrefixOps
HOL.Print
ppSymbolName
HOL.Print
PragmaCommand
HOL.OpenTheory.Article
Prec
HOL.Print
PrefixOp
HOL.Print
primitives
1 (Function)
HOL.Const
2 (Function)
HOL.TypeOp
Printable
HOL.Print
printKeyValue
HOL.OpenTheory.Package
productName
HOL.TypeOp
properSubsetName
HOL.Const
prov
1 (Function)
HOL.Const
2 (Function)
HOL.TypeOp
proveHyp
HOL.Rule
ProveHypCommand
HOL.OpenTheory.Article
push2Object
HOL.OpenTheory.Article
push2State
HOL.OpenTheory.Article
push3Object
HOL.OpenTheory.Article
push4Object
HOL.OpenTheory.Article
push5Object
HOL.OpenTheory.Article
push5State
HOL.OpenTheory.Article
pushObject
HOL.OpenTheory.Article
pushState
HOL.OpenTheory.Article
quoteName
HOL.Print
quoteNamespace
HOL.Print
rand
1 (Function)
HOL.Term
2 (Function)
HOL.Rule
3 (Function)
HOL.Conv
randUnsafe
HOL.Rule
range
HOL.Type
rator
1 (Function)
HOL.Term
2 (Function)
HOL.Rule
3 (Function)
HOL.Conv
ratorUnsafe
HOL.Rule
readArticle
1 (Function)
HOL.OpenTheory.Article
2 (Function)
HOL.OpenTheory
readBlock
HOL.OpenTheory.Package
readBlocks
HOL.OpenTheory.Package
readInterpretation
HOL.OpenTheory.Package
readList
HOL.OpenTheory.Package
readPackage
HOL.OpenTheory.Package
readPackageFile
HOL.OpenTheory.Package
readPackages
HOL.OpenTheory
readVersion
HOL.OpenTheory.Package
realNamespace
HOL.Name
RefCommand
HOL.OpenTheory.Article
refl
HOL.Thm
ReflCommand
HOL.OpenTheory.Article
refState
HOL.OpenTheory.Article
regularCommands
HOL.OpenTheory.Article
RemoveCommand
HOL.OpenTheory.Article
removeState
HOL.OpenTheory.Article
Rename
1 (Type/Class)
HOL.OpenTheory.Interpret
2 (Data Constructor)
HOL.OpenTheory.Interpret
renameAvoiding
HOL.Var
renameBoundVar
HOL.Subst
renameFresh
HOL.Term
Renames
1 (Type/Class)
HOL.OpenTheory.Interpret
2 (Data Constructor)
HOL.OpenTheory.Interpret
renameSymbol
HOL.OpenTheory.Interpret
RepConstProv
HOL.Data
repeat
HOL.Conv
Requires
1 (Type/Class)
HOL.OpenTheory.Package
2 (Data Constructor)
HOL.OpenTheory.Package
requires
HOL.OpenTheory.Package
Result
HOL.Conv
rhs
HOL.Term
rhsUnsafe
HOL.Term
RightAssoc
HOL.Print
sameType
HOL.Term
sameTypeVar
HOL.Term
select
HOL.Const
selectName
HOL.Const
Sequent
1 (Type/Class)
HOL.Sequent
2 (Data Constructor)
HOL.Sequent
sequentObject
HOL.OpenTheory.Article
sequents
HOL.Theory
setNamespace
HOL.Name
sharingSubst
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
singleton
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
singletonUnsafe
HOL.Subst
Size
HOL.Data
size
1 (Function)
HOL.TypeData
2 (Function)
HOL.Type
3 (Function)
HOL.TermData
4 (Function)
HOL.Term
source
HOL.OpenTheory.Package
spaceParser
HOL.Parse
stack
HOL.OpenTheory.Article
standard
HOL.Theory
standardAxiomName
HOL.TermAlpha
standardAxioms
1 (Function)
HOL.TermAlpha
2 (Function)
HOL.Sequent
3 (Function)
HOL.Thm
StartParseInteger
HOL.Parse
State
1 (Type/Class)
HOL.OpenTheory.Article
2 (Data Constructor)
HOL.OpenTheory.Article
stripAbs
HOL.Term
stripApp
HOL.Term
stripFun
HOL.Type
sub
HOL.Conv
subName
HOL.Const
subRealName
HOL.Const
subsetName
HOL.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
SubstCommand
HOL.OpenTheory.Article
sucName
HOL.Const
sumName
HOL.TypeOp
sumNamespace
HOL.Name
supportedCommand
HOL.OpenTheory.Article
sym
HOL.Rule
Symbol
HOL.OpenTheory.Interpret
symbolName
HOL.OpenTheory.Interpret
SymCommand
HOL.OpenTheory.Article
Term
1 (Type/Class)
HOL.Data
2 (Data Constructor)
HOL.Data
TermAlpha
1 (Type/Class)
HOL.TermAlpha
2 (Data Constructor)
HOL.TermAlpha
TermData
HOL.Data
TermId
HOL.Data
TermObject
HOL.OpenTheory.Article
thenc
HOL.Conv
theorems
HOL.OpenTheory.Article
Theory
1 (Type/Class)
HOL.Theory
2 (Data Constructor)
HOL.Theory
Thm
HOL.Thm
ThmCommand
HOL.OpenTheory.Article
thmMap
HOL.Theory
ThmObject
HOL.OpenTheory.Article
thms
HOL.Theory
thmState
HOL.OpenTheory.Article
toDoc
HOL.Print
toInfo
HOL.OpenTheory.Package
toObject
HOL.OpenTheory.Article
toRenames
HOL.OpenTheory.Interpret
toString
HOL.Print
toStringWith
HOL.Print
trans
HOL.Rule
TransCommand
HOL.OpenTheory.Article
transUnsafe
HOL.Rule
try
HOL.Conv
trySharingSubst
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
trySubst
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
tryTypeSubst
HOL.Subst
Type
1 (Type/Class)
HOL.Data
2 (Data Constructor)
HOL.Data
TypeData
HOL.Data
TypeId
HOL.Data
TypeObject
HOL.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
TypeOpCommand
HOL.OpenTheory.Article
TypeOpDef
1 (Type/Class)
HOL.Data
2 (Data Constructor)
HOL.Data
typeOpMap
HOL.Theory
TypeOpObject
HOL.OpenTheory.Article
TypeOpProv
HOL.Data
TypeOpSymbol
HOL.OpenTheory.Interpret
TypeSubst
1 (Type/Class)
HOL.TypeSubst
2 (Data Constructor)
HOL.TypeSubst
typeSubst
HOL.Subst
TypeVar
1 (Type/Class)
HOL.Data
2 (Data Constructor)
HOL.Data
Unchanged
HOL.Conv
UndefConstProv
HOL.Data
UndefTypeOpProv
HOL.Data
Union
HOL.OpenTheory.Package
union
HOL.Theory
unionList
HOL.Theory
unionName
HOL.Const
Var
1 (Type/Class)
HOL.Data
2 (Data Constructor)
HOL.Data
VarCommand
HOL.OpenTheory.Article
variantAvoiding
HOL.Name
VarObject
HOL.OpenTheory.Article
vars
HOL.TypeVar
varSubst
1 (Function)
HOL.TypeSubst
2 (Function)
HOL.Subst
VarTerm
HOL.Data
VarTermCommand
HOL.OpenTheory.Article
VarType
HOL.Data
VarTypeCommand
HOL.OpenTheory.Article
Version
1 (Type/Class)
HOL.OpenTheory.Article
2 (Type/Class)
HOL.OpenTheory.Package
3 (Data Constructor)
HOL.OpenTheory.Package
version
HOL.OpenTheory.Package
VersionCommand
HOL.OpenTheory.Article
versionCommand
HOL.OpenTheory.Article
zeroName
HOL.Const
ZeroParseInteger
HOL.Parse