# HG changeset patch
# User wenzelm
# Date 899480027 -7200
# Node ID 5c1f89ae8aefdb83352db3500dda6546e89a1eb1
# Parent  f7f5442c934a567085c9f45e5f4b82a9c5b54b33
moved String theory to main HOL;

diff -r f7f5442c934a -r 5c1f89ae8aef src/HOL/String.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/String.ML	Fri Jul 03 17:33:47 1998 +0200
@@ -0,0 +1,20 @@
+Goal "hd(''ABCD'') = CHR ''A''";
+by (Simp_tac 1);
+result();
+
+Goal "hd(''ABCD'') ~= CHR ''B''";
+by (Simp_tac 1);
+result();
+
+Goal "''ABCD'' ~= ''ABCX''";
+by (Simp_tac 1);
+result();
+
+Goal "''ABCD'' = ''ABCD''";
+by (Simp_tac 1);
+result();
+
+Goal
+  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
+by (Simp_tac 1);
+result();
diff -r f7f5442c934a -r 5c1f89ae8aef src/HOL/String.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/String.thy	Fri Jul 03 17:33:47 1998 +0200
@@ -0,0 +1,87 @@
+(*  Title:      HOL/String.thy
+    ID:         $Id$
+
+Hex chars and 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
+
+  (* chars *)
+
+  val zero = ord "0";
+  val ten = ord "A" - 10;
+
+  fun mk_nib n =
+    Syntax.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 =
+    Syntax.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 (xstr, _)] =
+        (case Syntax.explode_xstr xstr of
+          [c] => mk_char c
+        | _ => error ("Single character expected: " ^ xstr))
+    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
+
+  fun char_tr' (*"Char"*) [t1, t2] =
+        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
+    | char_tr' (*"Char"*) _ = raise Match;
+
+
+  (* strings *)
+
+  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
+    | mk_string (t :: ts) = Syntax.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 (xstr, _)] =
+        mk_string (map mk_char (Syntax.explode_xstr xstr))
+    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
+
+  fun cons_tr' (*"op #"*) [c, cs] =
+        Syntax.const "_String" $
+          Syntax.free (Syntax.implode_xstr (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;
diff -r f7f5442c934a -r 5c1f89ae8aef src/HOL/ex/String.ML
--- a/src/HOL/ex/String.ML	Fri Jul 03 11:02:01 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-Goal "hd(''ABCD'') = CHR ''A''";
-by (Simp_tac 1);
-result();
-
-Goal "hd(''ABCD'') ~= CHR ''B''";
-by (Simp_tac 1);
-result();
-
-Goal "''ABCD'' ~= ''ABCX''";
-by (Simp_tac 1);
-result();
-
-Goal "''ABCD'' = ''ABCD''";
-by (Simp_tac 1);
-result();
-
-Goal
-  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
-by (Simp_tac 1);
-result();
diff -r f7f5442c934a -r 5c1f89ae8aef src/HOL/ex/String.thy
--- a/src/HOL/ex/String.thy	Fri Jul 03 11:02:01 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-(*  Title:      HOL/String.thy
-    ID:         $Id$
-
-Hex chars and 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
-
-  (* chars *)
-
-  val zero = ord "0";
-  val ten = ord "A" - 10;
-
-  fun mk_nib n =
-    Syntax.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 =
-    Syntax.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 (xstr, _)] =
-        (case Syntax.explode_xstr xstr of
-          [c] => mk_char c
-        | _ => error ("Single character expected: " ^ xstr))
-    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
-
-  fun char_tr' (*"Char"*) [t1, t2] =
-        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
-    | char_tr' (*"Char"*) _ = raise Match;
-
-
-  (* strings *)
-
-  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
-    | mk_string (t :: ts) = Syntax.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 (xstr, _)] =
-        mk_string (map mk_char (Syntax.explode_xstr xstr))
-    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
-
-  fun cons_tr' (*"op #"*) [c, cs] =
-        Syntax.const "_String" $
-          Syntax.free (Syntax.implode_xstr (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;