# HG changeset patch
# User wenzelm
# Date 1001594140 -7200
# Node ID bebeb3b9e88e0d9e1146cf4498665457cc2da201
# Parent  f666c1e4133d9514c0b4765c4ea2c0f8acdf49f8
obsolete;

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 "";