From 55c148073df8de5f0cf4c45db23d2e3da7f4f093 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 20 Sep 2018 21:35:51 +0200
Subject: Derive can prove pathcomp_comp. Fix typo.

---
 HoTT_Base.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 0b460d9..9e8fee7 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -53,7 +53,7 @@ text \<open>
 Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination.
 One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 
-@{thm U_cumulative'} is an alternative rule used by the method \<open>lift\<close> in @{file HoTT_Methods.thy}.
+@{thm U_cumulative'} is an alternative rule used by the method \<open>cumulativity\<close> in @{file HoTT_Methods.thy}.
 \<close>
 
 
-- 
cgit v1.2.3