diff -r 408713c7f66b -r deec279dda0a ex/String.ML
--- /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();