From f88e1c0de030ac32014dd6f4f04fb4c6961b93ab Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 17 Jun 2018 20:37:33 +0200
Subject: Proof of projection functions now harder. Should look up automation
 methods.

---
 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 7794601..9b7c3e2 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -34,7 +34,7 @@ consts
   is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
 
 axiomatization where
-  inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U"
+  inhabited_implies_type: "\<And>a A. a : A \<Longrightarrow> A : U"
 
 
 section \<open>Type families\<close>
-- 
cgit v1.2.3