From 8e5bf7b358626b71ff5b7fdfeadf81c4910f38fd Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 29 Oct 2018 18:23:10 -0400
Subject: [PATCH] henglein tweak

---
 paper/gtt.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/paper/gtt.tex b/paper/gtt.tex
index c94b41a..be8c93c 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -9520,13 +9520,13 @@ Because of this, the theorems proven in that paper are more closely
 related to our model construction in section
 \ref{sec:contract}.
 %
-More specifically, many of the lemmas proven in the extended version
-of this paper \citep{newlicataahmed19:extended} have direct analogues
-in Henglein's work.
+More specifically, many of the properties of casts needed to prove
+theorem \ref{thm:axiomatic-graduality} have direct analogues
+in Henglein's work, such as the coherence theorems.
 %
 We have not included these lemmas in the paper because they are quite
-similar to lemmas proven in \citet{newahmed18}; see there for a
-more detailed comparison.
+similar to lemmas proven in \citet{newahmed18}; see there for a more
+detailed comparison, and the extended version of this paper for full proof details \citep{newlicataahmed19:extended}.
 %
 Finally, we note that our assumption of compositionality, i.e., that
 all casts can be decomposed into an upcast followed by a downcast, is
-- 
GitLab