author | wenzelm |
Tue, 16 Jan 2001 00:38:25 +0100 | |
changeset 10916 | df4a70b6ad7b |
parent 5199 | be986f7a6def |
child 11020 | 646c929b6293 |
permissions | -rw-r--r-- |
theory StringEx = Main: lemma "hd ''ABCD'' = CHR ''A''" by simp lemma "hd ''ABCD'' \<noteq> CHR ''B''" by simp lemma "''ABCD'' \<noteq> ''ABCX''" by simp lemma "''ABCD'' = ''ABCD''" by simp lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq> ''ABCDEFGHIJKLMNOPQRSTUVWXY''" by simp lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}" by (simp add: insert_commute) lemma "set ''Foobar'' = ?X" by (simp add: insert_commute) end