src/HOL/ex/String.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/String.ML	Wed Mar 22 12:42:34 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();