From ed41980ed5cee12d7c5eea2e40627e5a390a83f8 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 27 May 2020 21:31:57 +0200
Subject: minor

---
 hott/Identity.thy | 1 +
 1 file changed, 1 insertion(+)

(limited to 'hott/Identity.thy')

diff --git a/hott/Identity.thy b/hott/Identity.thy
index d664fbc..64aea5a 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -145,6 +145,7 @@ Lemma (derive) pathcomp_refl:
 
 definition [implicit]: "ru p \<equiv> pathcomp_refl ? ? ? p"
 definition [implicit]: "lu p \<equiv> refl_pathcomp ? ? ? p"
+
 translations
   "CONST ru p" \<leftharpoondown> "CONST pathcomp_refl A x y p"
   "CONST lu p" \<leftharpoondown> "CONST refl_pathcomp A x y p"
-- 
cgit v1.2.3