Index - S
| sameType | HOL.Term |
| sameTypeVar | HOL.Term |
| select | HOL.Const |
| selectName | HOL.Const |
| Sequent | |
| 1 (Type/Class) | HOL.Sequent |
| 2 (Data Constructor) | HOL.Sequent |
| sequentObject | HOL.OpenTheory.Article |
| sequents | HOL.Theory |
| setNamespace | HOL.Name |
| sharingSubst | |
| 1 (Function) | HOL.TypeSubst |
| 2 (Function) | HOL.Subst |
| singleton | |
| 1 (Function) | HOL.TypeSubst |
| 2 (Function) | HOL.Subst |
| singletonUnsafe | HOL.Subst |
| Size | HOL.Data |
| size | |
| 1 (Function) | HOL.TypeData |
| 2 (Function) | HOL.Type |
| 3 (Function) | HOL.TermData |
| 4 (Function) | HOL.Term |
| source | HOL.OpenTheory.Package |
| spaceParser | HOL.Parse |
| stack | HOL.OpenTheory.Article |
| standard | HOL.Theory |
| standardAxiomName | HOL.TermAlpha |
| standardAxioms | |
| 1 (Function) | HOL.TermAlpha |
| 2 (Function) | HOL.Sequent |
| 3 (Function) | HOL.Thm |
| StartParseInteger | HOL.Parse |
| State | |
| 1 (Type/Class) | HOL.OpenTheory.Article |
| 2 (Data Constructor) | HOL.OpenTheory.Article |
| stripAbs | HOL.Term |
| stripApp | HOL.Term |
| stripFun | HOL.Type |
| sub | HOL.Conv |
| subName | HOL.Const |
| subRealName | HOL.Const |
| subsetName | HOL.Const |
| Subst | |
| 1 (Type/Class) | HOL.Subst |
| 2 (Data Constructor) | HOL.Subst |
| subst | |
| 1 (Function) | HOL.TypeSubst |
| 2 (Function) | HOL.Subst |
| 3 (Function) | HOL.Thm |
| SubstCommand | HOL.OpenTheory.Article |
| sumName | HOL.TypeOp |
| sumNamespace | HOL.Name |
| supportedCommand | HOL.OpenTheory.Article |
| sym | HOL.Rule |
| Symbol | HOL.OpenTheory.Interpret |
| symbolName | HOL.OpenTheory.Interpret |
| SymCommand | HOL.OpenTheory.Article |