src/HOL/ex/StringEx.ML
changeset 5278 a903b66822e2
parent 5199 be986f7a6def
child 8035 84c5ce912b43
     1.1 --- a/src/HOL/ex/StringEx.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/ex/StringEx.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -15,7 +15,6 @@
     1.4  by (Simp_tac 1);
     1.5  result();
     1.6  
     1.7 -Goal
     1.8 -  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
     1.9 +Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
    1.10  by (Simp_tac 1);
    1.11  result();