--- a/src/HOL/ex/StringEx.thy Tue Jan 16 00:37:41 2001 +0100
+++ b/src/HOL/ex/StringEx.thy Tue Jan 16 00:38:25 2001 +0100
@@ -1,2 +1,25 @@
-StringEx = String
+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