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 /Equal.thy | |
parent | f602cb54b39b3c1bb4f755db09bdeeb2f31a9559 (diff) |
Not sure what advantage is provided by having eta-expanded forms in the rules. Removing for now.
Diffstat (limited to 'Equal.thy')
-rw-r--r-- | Equal.thy | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 |