From 2781c68f0fdb435827097efc497c2172d6050e50 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 2 Apr 2020 23:27:06 +0200
Subject: 1. make id function an abbrev. 2. fix reduce method

---
 spartan/theories/Identity.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'spartan/theories/Identity.thy')

diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy
index 0edf20e..19b8b7a 100644
--- a/spartan/theories/Identity.thy
+++ b/spartan/theories/Identity.thy
@@ -261,7 +261,7 @@ Lemma transport_comp [comps]:
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
   shows "trans P (refl a) \<equiv> id (P a)"
-  unfolding transport_def id_def by reduce
+  unfolding transport_def by reduce
 
 \<comment> \<open>TODO: Build transport automation!\<close>
 
-- 
cgit v1.2.3