src/HOL/ex/StringEx.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17388 495c799df31d
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (* $Id$ *)
     2 
     3 header {* String examples *}
     4 
     5 theory StringEx imports Main begin
     6 
     7 lemma "hd ''ABCD'' = CHR ''A''"
     8   by simp
     9 
    10 lemma "hd ''ABCD'' \<noteq> CHR ''B''"
    11   by simp
    12 
    13 lemma "''ABCD'' \<noteq> ''ABCX''"
    14   by simp
    15 
    16 lemma "''ABCD'' = ''ABCD''"
    17   by simp
    18 
    19 lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq>
    20   ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
    21   by simp
    22 
    23 lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}"
    24   by (simp add: insert_commute)
    25 
    26 lemma "set ''Foobar'' = ?X"
    27   by (simp add: insert_commute)
    28 
    29 end