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.

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

(limited to 'Sum.thy')

diff --git a/Sum.thy b/Sum.thy
index 463a9d4..2646c97 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -38,14 +38,14 @@ axiomatization where
   Sum_elim: "\<lbrakk>
     p: \<Sum>x:A. B x;
     C: \<Sum>x:A. B x \<longrightarrow> U i;
-    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) p: C p" and
+    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f p: C p" and
 
   Sum_comp: "\<lbrakk>
     a: A;
     b: B a;
     B: A \<longrightarrow> U i;
     C: \<Sum>x:A. B x \<longrightarrow> U i;
-    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) <a,b> \<equiv> f a b" and
+    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f <a,b> \<equiv> f a b" and
 
 \<comment> \<open>Congruence rules\<close>
 
-- 
cgit v1.2.3