summaryrefslogtreecommitdiff
path: root/language/l2.ott
diff options
context:
space:
mode:
Diffstat (limited to 'language/l2.ott')
-rw-r--r--language/l2.ott2
1 files changed, 2 insertions, 0 deletions
diff --git a/language/l2.ott b/language/l2.ott
index d6f8cfed..68131d52 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -928,6 +928,8 @@ terminals :: '' ::=
{{ tex < }}
| gt :: :: mathgt
{{ tex > }}
+ | ~= :: :: alphaeq
+ {{ tex \ensuremath{\approx} }}
| |- :: :: vdash
{{ tex \ensuremath{\vdash} }}
| |-t :: :: vdashT