Not sure what advantage is provided by having eta-expanded forms in the rules. Removing for now.

5 files changed, 12 insertions, 12 deletions

diff --git a/Coprod.thy b/Coprod.thy
index 431e103..b0a1ad2 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -28,19 +28,19 @@ where
     u: A + B;
     C: A + B \<longrightarrow> U i;
     \<And>x. x: A \<Longrightarrow> c x: C (inl x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda> x. c x) (\<lambda>y. d y) u: C u" and
+    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" and
 
   Coprod_comp_inl: "\<lbrakk>
     a: A;
     C: A + B \<longrightarrow> U i;
     \<And>x. x: A \<Longrightarrow> c x: C (inl x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inl a) \<equiv> c a" and
+    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a" and
 
   Coprod_comp_inr: "\<lbrakk>
     b: B;
     C: A + B \<longrightarrow> U i;
     \<And>x. x: A \<Longrightarrow> c x: C (inl x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inr b) \<equiv> d b"
+    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b"
 
 lemmas Coprod_form [form]
 lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim
diff --git a/Equal.thy b/Equal.thy
index 19e3939..99ff268 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -37,12 +37,12 @@ axiomatization where
     x: A;
     y: A;
     \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= f p : C x y p" and
 
   Equal_comp: "\<lbrakk>
     a: A;
     \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= f (refl a) \<equiv> f a"
 
 lemmas Equal_form [form]
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
diff --git a/Nat.thy b/Nat.thy
index 8a55852..657e790 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -28,18 +28,18 @@ where
     a: C 0;
     n: \<nat>;
     C: \<nat> \<longrightarrow> U i;
-    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a n: C n" and
+    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n" and
 
   Nat_comp_0: "\<lbrakk>
     a: C 0;
     C: \<nat> \<longrightarrow> U i;
-    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a 0 \<equiv> a" and
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" and
 
   Nat_comp_succ: "\<lbrakk>
     a: C 0;
     n: \<nat>;
     C: \<nat> \<longrightarrow> U i;
-    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
+    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
 
 lemmas Nat_form [form]
 lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
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>
 
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>