From 7a89ec1e72f61179767c6488177c6d12e69388c5 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 12 Aug 2018 13:04:16 +0200
Subject: Commit before testing polymorphic equality eliminator

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

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 614419e..e94ca5c 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -56,6 +56,7 @@ and
   U_cumulative: "\<And>A i j. \<lbrakk>A: U(i); i <- j\<rbrakk> \<Longrightarrow> A: U(j)"
     \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close>
 
+
 section \<open>Type families\<close>
 
 text "
-- 
cgit v1.2.3