aboutsummaryrefslogtreecommitdiff
path: root/spartan/core
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/core')
-rw-r--r--spartan/core/Spartan.thy4
1 files changed, 2 insertions, 2 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 3d59464..004ba8d 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -92,10 +92,10 @@ axiomatization where
eta: "f: \<Prod>x: A. B x \<Longrightarrow> \<lambda>x: A. f `x \<equiv> f" and
Pi_cong: "\<lbrakk>
+ \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x;
A: U i;
\<And>x. x: A \<Longrightarrow> B x: U i;
- \<And>x. x: A \<Longrightarrow> B' x: U i;
- \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x
+ \<And>x. x: A \<Longrightarrow> B' x: U i
\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x \<equiv> \<Prod>x: A. B' x" and
lam_cong: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x \<equiv> \<lambda>x: A. c x"