Notation can be introduced in Isabelle for both types and terms. Notation for a constant can be introduced where it is defined, later with an explicit notation (
notation), or locally in an Isar proof (
write). This is documented in isar-ref §8.2 §8.3.
Assigning correct priorities in mixfix declarations is crucial for avoiding syntactic ambiguities. Prefer to use templates (like
infixrfor binary operators)!
Use print modes (documented in isar-ref §8.1.3) to define notation that is only meant for convenient
input, or specific output scenarios (
When introducing notation that you consider standard or folklore, add a comment with a reference to some textbook, paper or Wikipedia entry to back your claim.
If you introduce new notation, put it into a bundle!
Bundles are documented in isar-ref §5.3. They can be either activated in a local theory context (
unbundle), in an Isar proof body (
include), in a proof refinement (
including), and in a context specification (
includes) (notably for
An example can be found in
A bundle can be unbundled on the toplevel only when the notation is specific enough (e.g. by a subscript) to rule out clashes with notation from other theories or future developments. A bundle for disabling the notation must be available regardless.
For syntax notations always provide both a bundle that enables it (
CONCEPT_syntax) and a bundle that disables it (
bundle timecredits_syntax begin notation timecredit_assn ("$") end bundle no_timecredits_syntax begin no_notation timecredit_assn ("$") end