From 77aa10763429d2ded040071fbf7bee331dd52f5e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 31 Jul 2020 18:10:10 +0200
Subject: (REF) Tweak attribute names in preparation for new logical
 introduction rule behavior

---
 hott/Identity.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'hott/Identity.thy')

diff --git a/hott/Identity.thy b/hott/Identity.thy
index d6efbf8..b9ebafb 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -41,7 +41,7 @@ axiomatization where
 
 lemmas
   [form] = IdF and
-  [intro, intros] = IdI and
+  [intr, intro] = IdI and
   [elim ?p ?a ?b] = IdE and
   [comp] = Id_comp and
   [refl] = IdI
@@ -567,7 +567,7 @@ interpretation \<Omega>2:
 notation \<Omega>2.horiz_pathcomp (infix "\<star>" 121)
 notation \<Omega>2.horiz_pathcomp' (infix "\<star>''" 121)
 
-Lemma [typechk]:
+Lemma [type]:
   assumes "\<alpha>: \<Omega>2 A a" and "\<beta>: \<Omega>2 A a"
   shows horiz_pathcomp_type: "\<alpha> \<star> \<beta>: \<Omega>2 A a"
     and horiz_pathcomp'_type: "\<alpha> \<star>' \<beta>: \<Omega>2 A a"
-- 
cgit v1.2.3