author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 11586 | d8a7f6318457 |
child 17388 | 495c799df31d |
permissions | -rw-r--r-- |
header {* String examples *} theory StringEx imports Main begin 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