diff options
| author | Clément Pit-Claudel | 2018-11-25 19:31:18 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-11-25 19:31:18 -0500 |
| commit | b400fa987dec3c2dabfd69ce305d3ab8f1dc8952 (patch) | |
| tree | a1bf762b871f654a02d175dbb86b5e87c392fff0 /doc/sphinx/user-extensions/syntax-extensions.rst | |
| parent | e0f55aecee2ed9fc6f56979c255688e08b136c20 (diff) | |
| parent | e367f1113738b28c42de6c87b7c9f3d0fce3f5be (diff) | |
Merge PR #9036: Add bodies to sphinx objects.
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 2214cbfb34..65df89da6c 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -31,8 +31,8 @@ Basic notations .. cmd:: Notation -A *notation* is a symbolic expression denoting some term or term -pattern. + A *notation* is a symbolic expression denoting some term or term + pattern. A typical notation is the use of the infix symbol ``/\`` to denote the logical conjunction (and). Such a notation is declared by |