aboutsummaryrefslogtreecommitdiff
path: root/Equal.thy
diff options
context:
space:
mode:
Diffstat (limited to 'Equal.thy')
-rw-r--r--Equal.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Equal.thy b/Equal.thy
index bd7dd93..11a966b 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -37,7 +37,7 @@ and
\<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x);
x: A;
y: A;
- p: a =\<^sub>A b
+ p: x =\<^sub>A y
\<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(p) : C(x)(y)(p)"
and
Equal_comp: "\<lbrakk>