diff -r f666c1e4133d -r bebeb3b9e88e src/HOL/ex/StringEx.ML
--- a/src/HOL/ex/StringEx.ML	Thu Sep 27 12:25:09 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-
-Goal "hd(''ABCD'') = CHR ''A''";
-by (Simp_tac 1);
-qed "";
-
-Goal "hd(''ABCD'') ~= CHR ''B''";
-by (Simp_tac 1);
-qed "";
-
-Goal "''ABCD'' ~= ''ABCX''";
-by (Simp_tac 1);
-qed "";
-
-Goal "''ABCD'' = ''ABCD''";
-by (Simp_tac 1);
-qed "";
-
-Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
-by (Simp_tac 1);
-qed "";