diff options
| author | Lars Hupel | 2018-09-18 16:52:08 +0200 |
|---|---|---|
| committer | Lars Hupel | 2018-09-18 16:52:08 +0200 |
| commit | f07e0e2349a222130209ada9c029eea3d1fe8144 (patch) | |
| tree | df5863f0fe5dd181dde689383a101bf3bb3f57e5 /EqualProps.thy | |
| parent | c93932c689640a530de946f35a0a9dc82e56e776 (diff) | |
add ROOT file
Diffstat (limited to '')
| -rw-r--r-- | EqualProps.thy | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index abb2623..f7a8d91 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -117,7 +117,6 @@ proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) fix x assume "x: A" show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r" \<comment> \<open>This requires substitution of *propositional* equality. \<close> - sorry oops |