--- a/thys2/SizeBound.thy	Thu Nov 04 13:52:17 2021 +0000
+++ b/thys2/SizeBound.thy	Tue Dec 14 16:06:42 2021 +0000
@@ -1580,7 +1580,17 @@
   using blexer_correctness main_main by auto
 
 
+
+export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
+
+
 unused_thms
 
 
+inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99)
+  where
+ "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) "
+
+
+
 end