--- a/thys3/Blexer.thy	Fri May 26 08:09:30 2023 +0100
+++ b/thys3/Blexer.thy	Fri May 26 08:10:17 2023 +0100
@@ -109,7 +109,7 @@
   by (smt append_Nil2 decode'_code old.prod.case)
 
 
-section {* Annotated Regular Expressions *}
+section \<open>Annotated Regular Expressions\<close>
 
 datatype arexp = 
   AZERO