diff -r a1421c88ae0a -r 34cd1d210b92 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Jul 01 20:47:16 2022 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Mon Jul 04 07:57:22 2022 +0000
@@ -68,4 +68,12 @@
 where
   "funny_funs fs = (\<lambda>x. x \<or> True) # (\<lambda>x. x \<or> False) # fs"
 
+text \<open>Explicit checks for strings etc.\<close>
+
+definition \<open>hello = ''Hello, world!''\<close>
+
+definition \<open>hello2 = String.explode (String.implode hello)\<close>
+
+definition \<open>which_hello \<longleftrightarrow> hello \<le> hello2\<close>
+
 end