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 |