From 7905c004780aba32f08ca9ec514f6bb85003b4aa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Feb 2016 22:43:49 +0100
Subject: [PATCH] LaTeX: change \set macros
---
docs/constructions.tex | 6 +++---
docs/setup.tex | 29 +++++++++--------------------
2 files changed, 12 insertions(+), 23 deletions(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 90aa83e42..679aeb007 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -249,7 +249,7 @@ Given a monoid $M$, we construct a monoid modeling someone owning an \emph{autho
(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
Let $\auth{M}$ be the monoid with carrier
\[
- \SET{ (x, \melt) }{ x \in \mcarp{\exm{\mcarp{M}}} \land \melt \in \mcarp{M} \land (x = \munit_{\exm{\mcarp{M}}} \lor \melt \leq_M x) }
+ \setComp{ (x, \melt) }{ x \in \mcarp{\exm{\mcarp{M}}} \land \melt \in \mcarp{M} \land (x = \munit_{\exm{\mcarp{M}}} \lor \melt \leq_M x) }
\]
and multiplication
\[
@@ -341,7 +341,7 @@ We first lift the transition relation to $\STSS \times \mathcal{P}(\STST)$ (impl
\begin{align*}
(s, T) \ra (s', T') \eqdef&\, s \ra s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
\textsf{frame}(s, T) \eqdef&\, (s, \STST \setminus (\STSL(s) \uplus T)) \\
- \upclose(S, T) \eqdef&\, \SET{ s' \in \STSS}{\exists s \in S.\; \textsf{frame}(s, T) \ststrans \textsf{frame}(s', T) }
+ \upclose(S, T) \eqdef&\, \setComp{ s' \in \STSS}{\exists s \in S.\; \textsf{frame}(s, T) \ststrans \textsf{frame}(s', T) }
\end{align*}
\noindent
@@ -358,7 +358,7 @@ This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s
Let $\STSMon{\STSS}$ be the monoid with carrier
\[
- \SET{ (s, S, T) \in \exm{\STSS} \times \mathcal{P}(\STSS) \times \mathcal{P}(\STST) }{ \begin{aligned} &(s = \munit \lor s \in S) \land \upclose(S, T) = S \land{} \\& S \neq \emptyset \land \All s \in S. \STSL(s) \sep T \end{aligned} }
+ \setComp{ (s, S, T) \in \exm{\STSS} \times \mathcal{P}(\STSS) \times \mathcal{P}(\STST) }{ \begin{aligned} &(s = \munit \lor s \in S) \land \upclose(S, T) = S \land{} \\& S \neq \emptyset \land \All s \in S. \STSL(s) \sep T \end{aligned} }
\]
and multiplication
\[
diff --git a/docs/setup.tex b/docs/setup.tex
index 14c27b93c..deb34faaf 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -152,9 +152,11 @@
\newcommand{\upclose}{\mathord{\uparrow}}
-\def\All #1.{\forall #1.\;}%
-\def\Exists #1.{\exists #1.\;}%
-\def\Ret #1.{#1.\;}%
+\newcommand{\spac}{\;} % a space
+
+\def\All #1.{\forall #1.\spac}%
+\def\Exists #1.{\exists #1.\spac}%
+\def\Ret #1.{#1.\spac}%
\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
\newcommand{\unitval}{()}%
@@ -182,21 +184,8 @@
\newcommand{\IF}{\mathrel{\text{if}}}
\newcommand{\WHEN}{\textrm{when }}
-
-
-\newcommand{\SET}[2]{
-\left\{%
-#1%
-\;\middle|\;%
-#2%
-\right\}
-}
-\newcommand{\SETB}[1]{
-\left\{%
-#1%
-\right\}
-}
-\newcommand{\SETC}[2]{#1 & #2}
+\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
+\newcommand*\set[1]{\left\{#1\right\}}
\newenvironment{inbox}[1][]{
\begin{array}[#1]{@{}l@{}}
@@ -317,8 +306,8 @@
%% various pieces of Syntax
\newcommand{\unitsort}{1}% \unit is bold.
-\def\MU #1.{\mu #1.\;}%
-\def\Lam #1.{\lambda #1.\;}%
+\def\MU #1.{\mu #1.\spac}%
+\def\Lam #1.{\lambda #1.\spac}%
\newcommand{\proves}{\vdash}
\newcommand{\provesalways}{\vdash_{\!\!\boxempty}}
--
GitLab