From f07e0e2349a222130209ada9c029eea3d1fe8144 Mon Sep 17 00:00:00 2001
From: Lars Hupel
Date: Tue, 18 Sep 2018 16:52:08 +0200
Subject: add ROOT file

---
 EqualProps.thy | 1 -
 1 file changed, 1 deletion(-)

(limited to 'EqualProps.thy')

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
 
 
-- 
cgit v1.2.3