diff options
| author | Josh Chen | 2018-09-19 11:57:22 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-09-19 11:57:22 +0200 |
| commit | 1305c6beca2448156b61649da1a719d055aaf7f7 (patch) | |
| tree | 81f1ea81350a70cfa27269c41f59e8640f9fd65a /Prod.thy | |
| parent | f602cb54b39b3c1bb4f755db09bdeeb2f31a9559 (diff) | |
Not sure what advantage is provided by having eta-expanded forms in the rules. Removing for now.
Diffstat (limited to 'Prod.thy')
| -rw-r--r-- | Prod.thy | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -20,8 +20,8 @@ axiomatization appl :: "[t, t] \<Rightarrow> t" ("(1_`/_)" [105, 106] 105) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax - "_prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_:_./ _)" 30) - "_prod_ascii" :: "[idt, t, t] \<Rightarrow> t" ("(3II _:_./ _)" 30) + "_prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_: _./ _)" 30) + "_prod_ascii" :: "[idt, t, t] \<Rightarrow> t" ("(3II _: _./ _)" 30) text \<open>The translations below bind the variable @{term x} in the expressions @{term B} and @{term b}.\<close> |