1.1 --- a/src/HOL/ex/StringEx.ML	Fri Nov 26 08:46:59 1999 +0100
     1.2 +++ b/src/HOL/ex/StringEx.ML	Mon Nov 29 11:21:30 1999 +0100
     1.3 @@ -1,20 +1,20 @@
     1.4  
     1.5  Goal "hd(''ABCD'') = CHR ''A''";
     1.6  by (Simp_tac 1);
     1.7 -result();
     1.8 +qed "";
     1.9  
    1.10  Goal "hd(''ABCD'') ~= CHR ''B''";
    1.11  by (Simp_tac 1);
    1.12 -result();
    1.13 +qed "";
    1.14  
    1.15  Goal "''ABCD'' ~= ''ABCX''";
    1.16  by (Simp_tac 1);
    1.17 -result();
    1.18 +qed "";
    1.19  
    1.20  Goal "''ABCD'' = ''ABCD''";
    1.21  by (Simp_tac 1);
    1.22 -result();
    1.23 +qed "";
    1.24  
    1.25  Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
    1.26  by (Simp_tac 1);
    1.27 -result();
    1.28 +qed "";