HOL.OpenTheory.Article
data Number
data Object
class Objective a
sequentObject
pushObject
push2Object
push3Object
push4Object
push5Object
popObject
pop2Object
pop3Object
pop4Object
pop5Object
data Command
regularCommands
type Version
supportedCommand
versionCommand
data State
pushState
push2State
push5State
popState
pop2State
pop3State
pop5State
peekState
defState
refState
removeState
thmState
initialState
executeCommand
type LineNumber
readArticle