CanSubst | |
1 (Type/Class) | HOL.TypeSubst |
2 (Type/Class) | HOL.Subst |
capturableVars | HOL.Subst |
Changed | HOL.Conv |
checksum | HOL.OpenTheory.Package |
closed | HOL.Var |
Command | HOL.OpenTheory.Article |
compose | |
1 (Function) | HOL.TypeSubst |
2 (Function) | HOL.OpenTheory.Interpret |
composeName | HOL.Const |
concatInfo | HOL.OpenTheory.Package |
concatRenames | HOL.OpenTheory.Interpret |
concl | |
1 (Function) | HOL.Sequent |
2 (Function) | HOL.Thm |
condName | HOL.Const |
conjName | HOL.Const |
ConsCommand | HOL.OpenTheory.Article |
consName | HOL.Const |
Const | |
1 (Type/Class) | HOL.Data |
2 (Data Constructor) | HOL.Data |
ConstCommand | HOL.OpenTheory.Article |
ConstDef | |
1 (Type/Class) | HOL.Data |
2 (Data Constructor) | HOL.Data |
constMap | HOL.Theory |
ConstObject | HOL.OpenTheory.Article |
ConstProv | HOL.Data |
consts | HOL.Const |
ConstSymbol | HOL.OpenTheory.Interpret |
ConstTerm | HOL.Data |
ConstTermCommand | HOL.OpenTheory.Article |
Conv | |
1 (Type/Class) | HOL.Conv |
2 (Data Constructor) | HOL.Conv |
crossName | HOL.Const |