From 1305c6beca2448156b61649da1a719d055aaf7f7 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 19 Sep 2018 11:57:22 +0200
Subject: Not sure what advantage is provided by having eta-expanded forms in
 the rules. Removing for now.

---
 Prod.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index f90ee9c..0bbe4ca 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -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>
 
-- 
cgit v1.2.3