1.1 --- a/src/HOL/Library/Code_Char.thy	Mon Oct 26 23:27:24 2009 +0100
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Tue Oct 27 15:32:20 2009 +0100
     1.3 @@ -35,4 +35,28 @@
     1.4  code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
     1.5    (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
     1.6  
     1.7 +
     1.8 +definition implode :: "string \<Rightarrow> String.literal" where
     1.9 +  "implode = STR"
    1.10 +
    1.11 +primrec explode :: "String.literal \<Rightarrow> string" where
    1.12 +  "explode (STR s) = s"
    1.13 +
    1.14 +lemma [code]:
    1.15 +  "literal_case f s = f (explode s)"
    1.16 +  "literal_rec f s = f (explode s)"
    1.17 +  by (cases s, simp)+
    1.18 +
    1.19 +code_reserved SML String
    1.20 +
    1.21 +code_const implode
    1.22 +  (SML "String.implode")
    1.23 +  (OCaml "failwith/ \"implode\"")
    1.24 +  (Haskell "_")
    1.25 +
    1.26 +code_const explode
    1.27 +  (SML "String.explode")
    1.28 +  (OCaml "failwith/ \"explode\"")
    1.29 +  (Haskell "_")
    1.30 +
    1.31  end