diff options
author | Josh Chen | 2019-03-26 17:04:01 +0100 |
---|---|---|
committer | Josh Chen | 2019-03-26 17:04:01 +0100 |
commit | 45c3879db6850282bc067318e31cccf42e60ac8f (patch) | |
tree | fd7753a339ee8a0e90bb97f80fc4105666ed7288 /Prod.thy | |
parent | 6dd1b27f7f84b17ad88e5b382042bd0c577a92f4 (diff) |
working towards biinv_imp_qinv
Diffstat (limited to '')
-rw-r--r-- | Prod.thy | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 |