Added Markus Wenzel's string representation.

--- a/ex/ROOT.ML	Wed Feb 01 17:18:00 1995 +0100
+++ b/ex/ROOT.ML	Fri Feb 03 16:19:45 1995 +0100
@@ -14,6 +14,7 @@
 time_use     "ex/cla.ML";
 time_use     "ex/meson.ML";
 time_use     "ex/mesontest.ML";
+time_use_thy "String";
 time_use_thy "InSort";
 time_use_thy "Qsort";
 time_use_thy "LexProd";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/String.ML	Fri Feb 03 16:19:45 1995 +0100
@@ -0,0 +1,22 @@
+val string_ss = list_ss addsimps (String.nibble.simps @ String.char.simps);
+
+goal String.thy "hd(''ABCD'') = CHR ''A''";
+by(simp_tac string_ss 1);
+result();
+
+goal String.thy "hd(''ABCD'') ~= CHR ''B''";
+by(simp_tac string_ss 1);
+result();
+
+goal String.thy "''ABCD'' ~= ''ABCX''";
+by(simp_tac string_ss 1);
+result();
+
+goal String.thy "''ABCD'' = ''ABCD''";
+by(simp_tac string_ss 1);
+result();
+
+goal String.thy
+  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
+by(simp_tac string_ss 1);
+result();

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/String.thy	Fri Feb 03 16:19:45 1995 +0100
@@ -0,0 +1,90 @@
+(*  Title:      HOL/String.thy
+    ID:         $Id$
+
+Hex chars. Strings.
+*)
+
+String = List +
+
+datatype
+  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
+         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
+
+datatype
+  char = Char (nibble, nibble)
+
+types
+  string = "char list"
+
+syntax
+  "_Char"       :: "xstr => char"       ("CHR _")
+  "_String"     :: "xstr => string"     ("_")
+
+end
+
+
+ML
+
+local
+  open Syntax;
+
+  val ssquote = enclose "''" "''";
+
+
+  (* chars *)
+
+  val zero = ord "0";
+  val ten = ord "A" - 10;
+
+  fun mk_nib n =
+    const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
+
+  fun dest_nib (Const (c, _)) =
+        (case explode c of
+          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
+        | _ => raise Match)
+    | dest_nib _ = raise Match;
+
+  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
+
+
+  fun mk_char c =
+    const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
+
+  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
+    | dest_char _ = raise Match;
+
+
+  fun char_tr (*"_Char"*) [Free (c, _)] =
+        if size c = 1 then mk_char c
+        else error ("Bad character: " ^ quote c)
+    | char_tr (*"_Char"*) ts = raise_term "char_tr" ts;
+
+  fun char_tr' (*"Char"*) [t1, t2] =
+        const "_Char" $ free (ssquote (dest_nibs t1 t2))
+    | char_tr' (*"Char"*) _ = raise Match;
+
+
+  (* strings *)
+
+  fun mk_string [] = const constrainC $ const "[]" $ const "string"
+    | mk_string (t :: ts) = const "op #" $ t $ mk_string ts;
+
+  fun dest_string (Const ("[]", _)) = []
+    | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
+    | dest_string _ = raise Match;
+
+
+  fun string_tr (*"_String"*) [Free (txt, _)] =
+        mk_string (map mk_char (explode txt))
+    | string_tr (*"_String"*) ts = raise_term "string_tr" ts;
+
+  fun cons_tr' (*"op #"*) [c, cs] =
+        const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs)))
+    | cons_tr' (*"op #"*) ts = raise Match;
+
+in
+  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
+  val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
+end;
+