diff -r 35a79fd062f7 -r d8a7f6318457 src/HOL/ex/StringEx.thy
--- a/src/HOL/ex/StringEx.thy	Thu Sep 27 15:42:01 2001 +0200
+++ b/src/HOL/ex/StringEx.thy	Thu Sep 27 15:42:08 2001 +0200
@@ -15,7 +15,8 @@
 lemma "''ABCD'' = ''ABCD''"
   by simp
 
-lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq> ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
+lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq>
+  ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
   by simp
 
 lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}"