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