One of the following logical judgment (which are in turn kinds of declaration):
- type declarations
- variant declarations
- function, relation, declared variable and individual declarations
- primitive axioms
- properties
- definition
- theory instantiation
- invariants
In a proof, primitive axioms and properties are automatically applied by the default tactic unless they are qualified by the explicit keyword, in which case they must be expicitly applied using the apply keyword, like compound judgments.