Index - T
| 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 |