--- a/src/HOL/Library/Code_Char.thy Mon Oct 26 23:27:24 2009 +0100
+++ b/src/HOL/Library/Code_Char.thy Tue Oct 27 15:32:20 2009 +0100
@@ -35,4 +35,28 @@
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
(Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
+
+definition implode :: "string \<Rightarrow> String.literal" where
+ "implode = STR"
+
+primrec explode :: "String.literal \<Rightarrow> string" where
+ "explode (STR s) = s"
+
+lemma [code]:
+ "literal_case f s = f (explode s)"
+ "literal_rec f s = f (explode s)"
+ by (cases s, simp)+
+
+code_reserved SML String
+
+code_const implode
+ (SML "String.implode")
+ (OCaml "failwith/ \"implode\"")
+ (Haskell "_")
+
+code_const explode
+ (SML "String.explode")
+ (OCaml "failwith/ \"explode\"")
+ (Haskell "_")
+
end