From fa413a91f73773c4cb9c83ed65837320b598e1d4 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 1 Mar 2019 20:44:02 +0100
Subject: finished proof of transport_biinv

---
 HoTT_Methods.thy | 1 -
 1 file changed, 1 deletion(-)

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index ad7384d..27f252b 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -70,7 +70,6 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}.
 method derive uses lems declares comp =
   (routine add: lems | compute add: lems comp: comp | cumulativity form: lems | hierarchy)+
 
-
 section \<open>Additional method combinators\<close>
 
 text \<open>
-- 
cgit v1.2.3