diff options
author | Josh Chen | 2018-09-20 14:14:17 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-20 14:14:17 +0200 |
commit | 0bceaa97dfc4899ec2489dc3f2cd2ea11f5ae358 (patch) | |
tree | b57993a0dd66b222ba02e5f1aed62f22bfa9a02f /Prod.thy | |
parent | 19eb191526ed6071ce4dbd44804122d53eea83c9 (diff) |
Application should bind tighter than composition
Diffstat (limited to '')
-rw-r--r-- | Prod.thy | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -17,7 +17,7 @@ section \<open>Basic definitions\<close> axiomatization Prod :: "[t, tf] \<Rightarrow> t" and lambda :: "(t \<Rightarrow> t) \<Rightarrow> t" (binder "\<^bold>\<lambda>" 30) and - appl :: "[t, t] \<Rightarrow> t" (infixl "`" 105) \<comment> \<open>Application binds tighter than abstraction.\<close> + appl :: "[t, t] \<Rightarrow> t" ("(1_`_)" [120, 121] 120) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax "_prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_: _./ _)" 30) |