From 2498c1512a81a9a73a5a8b6a1a0018ad824df778 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 23:57:38 +0200
Subject: Distinguish the typing judgment

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

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index a229e83..1110e14 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -23,8 +23,7 @@ text "
   For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it.
 "
 
-consts
-  has_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_:/ _)" [0, 0] 1000)
+judgment has_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_:/ _)" [0, 0] 1000)
 
 
 section \<open>Universe hierarchy\<close>
-- 
cgit v1.2.3