From 9ba47208278f7deea0dabed40a72fff89ecc5720 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 1 Mar 2019 20:05:00 +0100
Subject: change id precedence

---
 Prod.thy | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 2cb62e4..aeddc49 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -117,7 +117,9 @@ lemma compose_assoc:
   shows "(h o[B] g) o[A] f \<equiv> h o[A] g o[A] f"
 unfolding compose_def by (derive lems: assms cong)
 
-abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x"
+abbreviation id :: "t \<Rightarrow> t"  ("(id _)" [115] 114)  where "id A \<equiv> \<lambda>x: A. x"
+
+lemma id_type [intro]: "\<And>A. A: U i \<Longrightarrow> id A: A \<rightarrow> A" by derive
 
 
 section \<open>Universal quantification\<close>
-- 
cgit v1.2.3