diff options
author | Josh Chen | 2018-09-18 21:20:08 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-18 21:20:08 +0200 |
commit | 59a1409b1d15860344e91a4512b60ab8d4368e44 (patch) | |
tree | fe25a144dfac0727a71371176d3f63927407d2d9 /EqualProps.thy | |
parent | c93932c689640a530de946f35a0a9dc82e56e776 (diff) | |
parent | f9bbcffd4a45599c306815104dccb6b549b306ee (diff) |
Merge branch 'larsrh-topic/root'
Diffstat (limited to 'EqualProps.thy')
-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 |