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