# HG changeset patch
# User wenzelm
# Date 1745497416 -7200
# Node ID cf506179fc4c43404086538f7a29444b4d121d18
# Parent  794014f7eeeec71d20c72c407ab55597b71c64de
tuned document text;

diff -r 794014f7eeee -r cf506179fc4c src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy
--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Apr 24 12:23:37 2025 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Apr 24 14:23:36 2025 +0200
@@ -59,7 +59,7 @@
 
 test_code check in Scala
 
-text \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close>
+text \<open>Checking the index maximum for \<^verbatim>\<open>PolyML\<close>.\<close>
 
 qualified definition \<open>check_max = ()\<close>