--- 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