| occurs | Theory.Model, Theory |
| occursVTerm | Theory.Model, Theory |
| One | Theory.Model, Theory |
| OneLineMode | Theory.Text.Pretty |
| oneStepProver | Theory.Proof, Theory |
| opAction | Theory.Text.Pretty |
| opAt | Theory.Text.Parser.Token |
| opBang | Theory.Text.Parser.Token |
| opChain | Theory.Text.Parser.Token |
| opDedBefore | Theory.Text.Pretty |
| opDot | Theory.Text.Pretty |
| opEdge | Theory.Text.Pretty |
| openFormula | Theory.Model.Formula, Theory.Model, Theory |
| openFormulaPrefix | Theory.Model.Formula, Theory.Model, Theory |
| openGoals | Theory.Constraint.Solver.Goals |
| openGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| OpenTheory | Theory |
| openTheory | Theory |
| opEqual | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| Operator | Theory.Text.Pretty |
| operator | Theory.Text.Pretty |
| operator_ | Theory.Text.Pretty |
| opExists | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opExp | Theory.Text.Parser.Token |
| opForall | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opIff | Theory.Text.Pretty |
| opImp | Theory.Text.Pretty |
| opImplies | Theory.Text.Parser.Token |
| opLAnd | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opLeftarrow | Theory.Text.Parser.Token |
| opLEquiv | Theory.Text.Parser.Token |
| opLess | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opLFalse | Theory.Text.Parser.Token |
| opLNot | Theory.Text.Parser.Token |
| opLongleftarrow | Theory.Text.Parser.Token |
| opLongrightarrow | Theory.Text.Parser.Token |
| opLOr | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opLTrue | Theory.Text.Parser.Token |
| opMinus | Theory.Text.Parser.Token |
| opMult | Theory.Text.Parser.Token |
| opParens | Theory.Text.Pretty |
| opPath | Theory.Text.Pretty |
| opPlus | Theory.Text.Parser.Token |
| opProvides | Theory.Text.Pretty |
| opRequires | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opRightarrow | Theory.Text.Parser.Token |
| opSharp | Theory.Text.Parser.Token |
| opSlash | Theory.Text.Parser.Token |
| Or | Theory.Model.Formula, Theory.Model, Theory |
| orelse | Theory.Proof, Theory |
| OutFact | Theory.Model.Fact, Theory.Model, Theory |
| outFact | Theory.Model.Fact, Theory.Model, Theory |