aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Prod.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Prod.thy b/Prod.thy
index aeddc49..75db657 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -15,7 +15,7 @@ section \<open>Basic type definitions\<close>
axiomatization
Prod :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and
lam :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and
- app :: "[t, t] \<Rightarrow> t" ("(2_`_)" [120, 121] 120)
+ app :: "[t, t] \<Rightarrow> t" ("(2_`/_)" [120, 121] 120)
\<comment> \<open>Application should bind tighter than abstraction.\<close>
syntax