From 42624c947418c39eb22f07559e3b22442ccc43a2 Mon Sep 17 00:00:00 2001
From: Jeehoon Kang <jeehoon.kang@sf.snu.ac.kr>
Date: Sun, 14 Aug 2016 16:13:19 +0900
Subject: [PATCH] docs: fix bug in ghost resource laws
---
docs/logic.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/logic.tex b/docs/logic.tex
index 01d904d71..a8e7552ad 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -417,7 +417,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\begin{mathpar}
\begin{array}{rMcMl}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff& \ownGGhost{\melt \mtimes \meltB} \\
-\ownGGhost{\melt} &\provesIff& \mval(\melt) \\
+\ownGGhost{\melt} &\proves& \mval(\melt) \\
\TRUE &\proves& \ownGGhost{\munit}
\end{array}
\and
--
GitLab