From 8d0ef7c51af315f03600a98e4e05dee1f009d503 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 17 Apr 2019 18:00:48 +0200
Subject: [PATCH] Label new rule
If Ralf didn't know it, I guess it deserves a name. This is the first I got,
feel free to improve.
---
docs/ghost-state.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 224999e23..169dcfaeb 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -64,7 +64,7 @@ In other words, when working below the except-0 modality, we can \emph{strip
away} the later from timeless propositions. In fact, we can strip away later
from timeless propositions even when working under the later modality:
\begin{mathpar}
- \infer{\timeless{\prop} \and \prop \proves \later \propB}
+ \inferH{later-timeless-strip}{\timeless{\prop} \and \prop \proves \later \propB}
{\later\prop \proves \later\propB}
\end{mathpar}
This rule looks different from the above ones, because we still do not have that
--
GitLab