From f602cb54b39b3c1bb4f755db09bdeeb2f31a9559 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 19 Sep 2018 11:55:45 +0200
Subject: proof of associativity of path composition

---
 HoTT_Base.thy | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 69cc1b1..0b460d9 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -25,9 +25,14 @@ axiomatization
   lt  :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999) and
   leq :: "[ord, ord] \<Rightarrow> prop"  (infix "\<le>" 999)
 where
-  lt_Suc [intro]: "n < (Suc n)" and
-  lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
-  leq_min [intro]: "O \<le> n"
+  lt_Suc: "n < (Suc n)" and
+  lt_trans: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
+  leq_min: "O \<le> n"
+
+declare
+  lt_Suc [intro!]
+  leq_min [intro!]
+  lt_trans [intro]
 
 
 section \<open>Judgment\<close>
-- 
cgit v1.2.3