diff -r f04b33ce250f -r a4dc62a46ee4 ex/String.ML
--- a/ex/String.ML	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-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();