# HG changeset patch
# User haftmann
# Date 1256653940 -3600
# Node ID a5eba04475594b9c351374f09c24e65e72cc2edd
# Parent  ecb5cd453ef224382231ace451b9d1766f50aa15
added implode and explode

diff -r ecb5cd453ef2 -r a5eba0447559 src/HOL/Library/Code_Char.thy
--- 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