diff options
author | Josh Chen | 2018-08-18 00:06:20 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-18 00:06:20 +0200 |
commit | 29e9582b167c74b8e367e3226f63e12a25255b72 (patch) | |
tree | 6a0518e3fc01ea9aad502d96332707ef490a1151 /Equal.thy | |
parent | 9a0415ede2338b55ca9f4740e2a047c82e845443 (diff) |
Fixed mistake in Equal_elim and proof of rpathcomp_comp
Diffstat (limited to 'Equal.thy')
-rw-r--r-- | Equal.thy | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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> |