--- a/ChengsongTanPhdThesis/Chapters/Chapter2.tex	Mon May 09 17:24:26 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Chapter2.tex	Tue May 17 00:54:29 2022 +0100
@@ -214,7 +214,7 @@
 same trick as we did for the correctness proof,
 but this time we will have stronger equalities established.
 \subsection{"hrewrite" relation}
-List of simplifications for regular expressions simplification without bitcodes:
+List of 1-step rewrite rules for regular expressions simplification without bitcodes:
 \
 
 

--- a/thys2/blexer2.sc	Mon May 09 17:24:26 2022 +0100
+++ b/thys2/blexer2.sc	Tue May 17 00:54:29 2022 +0100
@@ -10,7 +10,7 @@
 //
 //   amm lexer.sc all
 
-import scala.util.Try
+
 
 // regular expressions including records
 abstract class Rexp 
@@ -60,6 +60,8 @@
 case class ANOT(bs: Bits, r: ARexp) extends ARexp
 case class AANYCHAR(bs: Bits) extends ARexp
 
+import scala.util.Try
+
 trait Generator[+T] {
     self => // an alias for "this"
     def generate(): T