Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated
authorChristian Urban <urbanc@in.tum.de>
Wed, 18 Sep 2019 16:35:57 +0100
changeset 358 06aa99b54423
parent 357 533765dc71cc
child 359 fedc16924b76
updated
thys/BitCoded2.thy file | annotate | diff | comparison | revisions 
--- 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"
lexing