enterTheory

open fun enterTheory(ctx: TheoryContext)