diff --git a/src/Glossary.v b/src/Glossary.v
index 1bdc1bd..ebf9980 100644
--- a/src/Glossary.v
+++ b/src/Glossary.v
@@ -5,18 +5,18 @@
 
   $$\mathit{[start, limit) := \{n | start \leq n \lt limit\}}$$
 
-  In other words, start is included, and limit is excluded.
+  In other words, start of the range is included, and limit is excluded.
 
-- Accessing subranges of a binary representation of a number is denoted with $\{\}$.
-  For example, this denotes a binary number obtained by taking bits from 128-th
-  to 255-th, both inclusive, of the value $\mathit{op}$:
+- Accessing subranges of a binary representation of a number is denoted with $\{low, high\}$.
+  For example, this denotes a binary number obtained by taking bits from 128-th inclusive to
+  to 256-th exclusive of the value $\mathit{op}$:
 
-  $$\mathit{op}\{255, 128\}$$
+  $$\mathit{op}\{128, 256\}$$
 
-- Concatenation of sequences of binary numbers is denoted with $||$
+- Concatenation of sequences of binary numbers is denoted with $\#\#$
 
-  For example, this denotes concatenating bit representations of the numbers $a$ and $b$:
-  $$a || b$$
+  For example, the following denotes concatenating bit representations of the numbers $a$ and $b$:
+  $$a \#\# b$$
 *)
 
 (**
diff --git a/src/sem/PtrAdd.v b/src/sem/PtrAdd.v
index 0890e70..15f5c26 100644
--- a/src/sem/PtrAdd.v
+++ b/src/sem/PtrAdd.v
@@ -41,7 +41,7 @@ $$\mathit{ptr_{out}} := \mathit{ptr_{in}} | _\mathit{offset := offset + diff}$$
 
 6. Store the result, tagged as a pointer, to `out`. The most significant 128 bits of result are taken from `op1`, the least significant bits hold an encoded pointer:
 
-$$result := \mathit{op_1}\{255\dots128\} || \texttt{encode}(\mathit{ptr_{out}})$$
+$$result := \mathit{op_1}\{255\dots128\} \#\# \texttt{encode}(\mathit{ptr_{out}})$$
 
    *)
   Inductive step_ptradd : instruction -> smallstep :=
diff --git a/src/sem/PtrPack.v b/src/sem/PtrPack.v
index a5ec9c3..dc8ca49 100644
--- a/src/sem/PtrPack.v
+++ b/src/sem/PtrPack.v
@@ -31,7 +31,7 @@ See Usage.
 3. Ensure that the lower 128 bits of $\mathit{op}_2$ are zero. Otherwise panic.
 4. Store the result, tagged as a pointer, to `out`:
 
-$$result := \mathit{op_1}\{255\dots128\} || \mathit{op_2}\{128\dots 0\}$$
+$$result := \mathit{op_1}\{255\dots128\} \#\# \mathit{op_2}\{128\dots 0\}$$
    *)
 
   | step_PtrPack :
diff --git a/src/sem/PtrShrink.v b/src/sem/PtrShrink.v
index 7a749bb..f4950f3 100644
--- a/src/sem/PtrShrink.v
+++ b/src/sem/PtrShrink.v
@@ -40,7 +40,7 @@ $$\mathit{ptr_{out}} := \mathit{ptr_{in}} | _\mathit{length := length - diff}$$
 
 6. Store the result, tagged as a pointer, to `out`:
 
-$$result := \mathit{op_1}\{255\dots128\} || \texttt{encode}(\mathit{ptr_{out}})$$
+$$result := \mathit{op_1}\{255\dots128\} \#\# \texttt{encode}(\mathit{ptr_{out}})$$
    *)
 
   | step_PtrShrink :
diff --git a/src/sem/PtrSub.v b/src/sem/PtrSub.v
index 83821c5..356b89e 100644
--- a/src/sem/PtrSub.v
+++ b/src/sem/PtrSub.v
@@ -52,7 +52,7 @@ $$\mathit{ptr_{out}} := \mathit{ptr_{in}} | _\mathit{offset := offset - diff}$$
 
 6. Store the result, tagged as a pointer, to `out`. The most significant 128 bits of result are taken from `op1`, the least significant bits hold an encoded pointer:
 
-$$result := \mathit{op_1}\{255\dots128\} || \texttt{encode}(\mathit{ptr_{out}})$$
+$$result := \mathit{op_1}\{255\dots128\} \#\# \texttt{encode}(\mathit{ptr_{out}})$$
 
    *)
   Inductive step_ptrsub : instruction -> smallstep :=