diff --git a/CHANGELOG.md b/CHANGELOG.md
index b3463405bf38b76cc197a1123282cd6e995485f8..1d5395f2079f2daabf6e89e6b65927708af21bc0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,9 +5,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
## Iris 3.0 (unfinished)
-* There now is a deprecation process. The modules `*.deprecated`
- contain deprecated notations and definitions that are provided for
- backwards compatibility and will be removed in a future version of Iris.
+* There now is a deprecation process. The modules `*.deprecated` contain
+ deprecated notations and definitions that are provided for backwards
+ compatibility and will be removed in a future version of Iris.
* View shifts are radically simplified to just internalize frame-preserving
updates. Weakestpre is defined inside the logic, and invariants and view
shifts with masks are also coded up inside Iris. Adequacy of weakestpre is
@@ -23,11 +23,11 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Renaming and moving things around: uPred and the rest of the base logic are
in `base_logic`, while `program_logic` is for everything involving the
general Iris notion of a language.
-* [#] Slightly weaker notion of atomicity: an expression is atomic if it reduces
- in one step to something that does not reduce further.
-* Changed notation for embedding Coq assertions into Iris. The new notation
- is ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope.
- (The old notations are provided in `base_logic.deprecated`.)
+* Slightly weaker notion of atomicity: an expression is atomic if it reduces in
+ one step to something that does not reduce further.
+* Changed notation for embedding Coq assertions into Iris. The new notation is
+ ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope. (The old notations are
+ provided in `base_logic.deprecated`.)
* Up-closure of namespaces is now a notation (↑) instead of a coercion.
* With invariants and the physical state being handled in the logic, there
is no longer any reason to demand the CMRA unit to be discrete.
diff --git a/docs/language.tex b/docs/language.tex
index ad097eb74756867909399b362bf94b969cc17503..4b34ed2d8893b243e5fe17d8d95a1470a2a5a73e 100644
--- a/docs/language.tex
+++ b/docs/language.tex
@@ -2,7 +2,7 @@
\label{sec:language}
A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), and a nonempty set \State of \emph{states} (metavariable $\state$) such that
-\begin{itemize}
+\begin{itemize}[itemsep=0pt]
\item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \Val$ (notice the latter is partial), such that
\begin{mathpar}
{\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and
@@ -21,8 +21,8 @@ A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metav
\end{defn}
\begin{defn}
- An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value:
- \[ \All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
+ An expression $\expr$ is \emph{atomic} if it reduces in one step to something irreducible:
+ \[ \All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \lnot \red(\expr_2, \state_2) \]
\end{defn}
\begin{defn}[Context]
@@ -55,3 +55,8 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \vec\expr}{\state_2}}
\end{mathpar}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End: