changeset 37459 | 7a3610dca96b |
parent 37222 | 4d984bc33c66 |
child 38857 | 97775f3e8722 |
--- a/src/HOL/Library/Code_Char.thy Fri Jun 18 15:03:20 2010 +0200 +++ b/src/HOL/Library/Code_Char.thy Fri Jun 18 15:03:20 2010 +0200 @@ -58,12 +58,12 @@ (SML "String.implode") (OCaml "failwith/ \"implode\"") (Haskell "_") - (Scala "List.toString((_))") + (Scala "!(\"\" ++/ _)") code_const explode (SML "String.explode") (OCaml "failwith/ \"explode\"") (Haskell "_") - (Scala "List.fromString((_))") + (Scala "!(_.toList)") end