# HG changeset patch
# User wenzelm
# Date 943870890 -3600
# Node ID 84c5ce912b43b512ba566b23b3486219db89109c
# Parent  6fc37b5c5e9827b982af772aa265256272b81ffb
qed "";

diff -r 6fc37b5c5e98 -r 84c5ce912b43 src/HOL/ex/StringEx.ML
--- 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 "";