thys3/LexerSimp.thy
changeset 642 6c13f76c070b
parent 495 f9cdc295ccf7
--- a/thys3/LexerSimp.thy	Wed Feb 15 11:52:22 2023 +0000
+++ b/thys3/LexerSimp.thy	Thu Feb 16 23:23:22 2023 +0000
@@ -2,7 +2,7 @@
   imports "Lexer" 
 begin
 
-section {* Lexer including some simplifications *}
+section \<open>Lexer including some simplifications\<close>
 
 
 fun F_RIGHT where