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