diff -r 533765dc71cc -r 06aa99b54423 thys/BitCoded2.thy
--- a/thys/BitCoded2.thy	Tue Sep 17 08:42:13 2019 +0100
+++ b/thys/BitCoded2.thy	Wed Sep 18 16:35:57 2019 +0100
@@ -4014,8 +4014,7 @@
       apply(subst (asm) bder_simp_contains_IFF)
        apply(simp)
   
-  
-
+(* TOBE PROVED *)
 lemma
   assumes "s \<in> L (erase r)"
   shows "bders_simp r s >> bs \<longleftrightarrow> bders r s >> bs"