Mercurial Mercurial > hg > lexing / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys3/src/BlexerSimp.thy
changeset 569 5af61c89f51e
parent 563 c92a41d9c4da
child 570 3ed514e2d93c 
--- a/thys3/src/BlexerSimp.thy	Sat Jul 16 18:34:46 2022 +0100
+++ b/thys3/src/BlexerSimp.thy	Sun Jul 17 13:07:05 2022 +0100
@@ -106,8 +106,6 @@
   apply(induct r rule: bnullable.induct) 
         apply(auto)
   apply (metis append.assoc bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4))  
-   apply(case_tac n)
-  apply(auto)
   done
 
 lemma bmkepss_fuse:
lexing