diff options
author | Josh Chen | 2019-03-01 20:05:00 +0100 |
---|---|---|
committer | Josh Chen | 2019-03-01 20:05:00 +0100 |
commit | 9ba47208278f7deea0dabed40a72fff89ecc5720 (patch) | |
tree | ceed7267b68ebc156285d7edcae7cc11dc5a458b /Prod.thy | |
parent | 85fc133fa0d64c61c380fcecada8f8358ad4b773 (diff) |
change id precedence
Diffstat (limited to '')
-rw-r--r-- | Prod.thy | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -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> |