| changeset 11586 | d8a7f6318457 |
| parent 11020 | 646c929b6293 |
| child 16417 | 9bc16273c2d4 |
--- 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''}"