# HG changeset patch
# User Chengsong
# Date 1566228178 -3600
# Node ID abf178a5db58a2d2d9ed49d0e79d7501c7693f88
# Parent  6c71db65bdec9a1a4e25ab20a87a00856cefb793
hope it works

diff -r 6c71db65bdec -r abf178a5db58 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Mon Aug 19 13:33:53 2019 +0100
+++ b/thys/BitCoded.thy	Mon Aug 19 16:22:58 2019 +0100
@@ -1,5 +1,5 @@
 
-theory BitCoded
+theory BitCodedCT
   imports "Lexer" 
 begin
 
@@ -2756,7 +2756,7 @@
   shows " \<exists> a aa list. y = a#aa#list"
   by (metis Nil_is_map_conv arexp.simps(13) assms bsimp_AALTs.elims flts1 good.simps(5) good1 k0a)
 
-
+(*SAD*)
 (*this does not hold actually
 lemma bsimp_equiv0:
   shows "bsimp(bsimp r) = bsimp(bsimp (AALTs []  [r]))"
@@ -2881,7 +2881,7 @@
   shows"map f [a,b] = [f a, f b]"
   apply simp
   done
-
+(*SAD*)
 (* bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) =
        bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))*)
 (*This equality does not hold*)