--- a/thys3/Blexer.thy	Wed Feb 15 11:52:22 2023 +0000
+++ b/thys3/Blexer.thy	Thu Feb 16 23:23:22 2023 +0000
@@ -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