# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1568820957 -3600
# Node ID 06aa99b5442317b270d903ca35ba30127056ecd9
# Parent  533765dc71cc434c0a711063ffcd3bd32c60a5ec
updated

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"