From 0036345412d5c145b63693ed672b175018fa3791 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 22 Feb 2019 19:43:53 +0100
Subject: Proof of pathcomp associativity done. Some comments

---
 HoTT_Typing.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'HoTT_Typing.thy')

diff --git a/HoTT_Typing.thy b/HoTT_Typing.thy
index 6433139..ec7456e 100644
--- a/HoTT_Typing.thy
+++ b/HoTT_Typing.thy
@@ -27,7 +27,7 @@ section \<open>Terms and typing\<close>
 
 typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 
-judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
+judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_ :/ _)")
 
 
 section \<open>Typing functionality\<close>
-- 
cgit v1.2.3