aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy
diff options
context:
space:
mode:
Diffstat (limited to 'Prod.thy')
-rw-r--r--Prod.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Prod.thy b/Prod.thy
index a37fdd6..8d840bd 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -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)