diff -r 6756b026c5fe -r ee1caac29bb2 thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Fri Feb 08 12:47:35 2019 +0000
+++ b/thys/Sulzmann.thy	Sun Feb 10 21:53:57 2019 +0000
@@ -318,61 +318,5 @@
 qed
 
 
-lemma
-  "[a, a, a, a] \<in> (STAR(STAR(CHAR(a)))) \<rightarrow> 
-     (Stars [(Stars [Char a, Char a, Char a, Char a])])"
-  oops
-
-lemma
-  "([a,a] @ []) \<in> (STAR(STAR(CHAR(a)))) \<rightarrow> 
-     (Stars [(Stars [Char a, Char a])])"
-  apply(rule Posix.intros)
-  defer
-  apply (simp add: Posix_STAR2)
-  apply(simp)
-  apply(auto)[1]
-  apply(rule_tac s="[a] @ [a]" in subst)
-  apply(simp)
-  apply(rule Posix_STAR1)
-  apply(rule Posix_CHAR)
-  apply(rule_tac s="[a] @ []" in subst)
-  apply(simp)
-  apply(rule Posix_STAR1)
-       apply(rule Posix_CHAR)
-      apply(rule Posix_STAR2)
-     apply(simp)
-    apply(auto)
-  done
-
-
-lemma "lexer (STAR(STAR(CHAR(a)))) [a, a] = XXX"
-  apply(simp)
-  oops
-
-
-
-
-
-fun simp where
-  "simp (AALT bs a AZERO) = fuse bs (simp a)"
-| "simp (AALT bs AZERO a) = fuse bs (simp a)"
-| "simp (ASEQ bs a AZERO) = AZERO"
-| "simp (ASEQ bs AZERO a) = AZERO"
-| "simp a = a"
-
-
-
-
-
-
-
-definition blexers where
- "blexer r s \<equiv> if bnullable (bders (intern r) s) then 
-                decode (bmkeps (bders (intern r) s)) r else None"
-
-unused_thms
-
-
-
 
 end
\ No newline at end of file