qed "";

--- a/src/HOL/ex/StringEx.ML	Fri Nov 26 08:46:59 1999 +0100
+++ b/src/HOL/ex/StringEx.ML	Mon Nov 29 11:21:30 1999 +0100
@@ -1,20 +1,20 @@
 
 Goal "hd(''ABCD'') = CHR ''A''";
 by (Simp_tac 1);
-result();
+qed "";
 
 Goal "hd(''ABCD'') ~= CHR ''B''";
 by (Simp_tac 1);
-result();
+qed "";
 
 Goal "''ABCD'' ~= ''ABCX''";
 by (Simp_tac 1);
-result();
+qed "";
 
 Goal "''ABCD'' = ''ABCD''";
 by (Simp_tac 1);
-result();
+qed "";
 
 Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
 by (Simp_tac 1);
-result();
+qed "";