# HG changeset patch
# User wenzelm
# Date 979601905 -3600
# Node ID df4a70b6ad7b41469625d0acaead8d9d64a998c6
# Parent  6b66a8a530ce6f63d9b48f2b3ef20aeb4523c5b2
tuned examples;

diff -r 6b66a8a530ce -r df4a70b6ad7b src/HOL/ex/StringEx.thy
--- 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